From db9765d7f11a9c0ad6fb2620aff67cef7d8ab27b Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 21 May 2010 22:09:56 +0000
Subject: Dafny: Allow < and > for comparisons of datatype values (which then
 compares their ranks)

---
 Test/dafny0/Substitution.dfy | 4 ++--
 Test/dafny0/SumOfCubes.dfy   | 4 ----
 2 files changed, 2 insertions(+), 6 deletions(-)

(limited to 'Test/dafny0')

diff --git a/Test/dafny0/Substitution.dfy b/Test/dafny0/Substitution.dfy
index 9668afb9..72415fea 100644
--- a/Test/dafny0/Substitution.dfy
+++ b/Test/dafny0/Substitution.dfy
@@ -69,7 +69,7 @@ static function Substitute(e: Expression, v: int, val: int): Expression
 
 static function SubstSeq(/*ghost*/ parent: Expression,
                          q: seq<Expression>, v: int, val: int): seq<Expression>
-  requires (exists op,args :: parent == #Expression.Nary(op, args) && q <= args);
+  requires (forall a :: a in q ==> a < parent);
   decreases parent, false, q;
 {
   if q == [] then [] else
@@ -107,7 +107,7 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int)
 
 static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>,
                                     v: int, val: int)
-  requires (exists op,args :: parent == #Expression.Nary(op, args) && q <= args);
+  requires (forall a :: a in q ==> a < parent);
   ensures |SubstSeq(parent, q, v, val)| == |q|;
   ensures (forall k :: 0 <= k && k < |q| ==>
             SubstSeq(parent, q, v, val)[k] == Substitute(q[k], v, val));
diff --git a/Test/dafny0/SumOfCubes.dfy b/Test/dafny0/SumOfCubes.dfy
index e5fe9473..b4fab490 100644
--- a/Test/dafny0/SumOfCubes.dfy
+++ b/Test/dafny0/SumOfCubes.dfy
@@ -33,7 +33,6 @@ class SumOfCubes {
     while (k < m) 
       invariant n <= k && k <= m;
       invariant SumEmDown(0, n) + SumEmDown(n, k) == SumEmDown(0, k);
-      decreases m - k;
     {
       k := k + 1;
     }
@@ -65,7 +64,6 @@ class SumOfCubes {
     while (i < k)
       invariant i <= k;
       invariant SumEmDown(0, i) == GSum(i) * GSum(i);
-      decreases k - i;
     {
       call Lemma2(i);
       i := i + 1;
@@ -81,7 +79,6 @@ class SumOfCubes {
     while (i < k)
       invariant i <= k;
       invariant 2 * GSum(i) == i * (i - 1);
-      decreases k - i;
     {
       i := i + 1;
     }
@@ -102,7 +99,6 @@ class SumOfCubes {
     while (k < m)
       invariant n <= k && k <= m;
       invariant SumEmUp(n, m) == SumEmDown(n, k) + SumEmUp(k, m);
-      decreases m - k;
     {
       k := k + 1;
     }
-- 
cgit v1.2.3