diff options
| -rw-r--r-- | Dafny/Translator.ssc | 115 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b1.dfy | 122 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b2.dfy | 1 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b3.dfy | 2 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b8.dfy | 3 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 68 | ||||
| -rw-r--r-- | Test/dafny0/Definedness.dfy | 3 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 21 | ||||
| -rw-r--r-- | Test/dafny0/Termination.dfy | 58 | ||||
| -rw-r--r-- | Test/dafny0/Use.dfy | 1 | ||||
| -rw-r--r-- | Test/dafny1/SchorrWaite.dfy | 1 | ||||
| -rw-r--r-- | Test/dafny1/Substitution.dfy | 1 | ||||
| -rw-r--r-- | Test/vacid0/SparseArray.dfy | 2 |
13 files changed, 283 insertions, 115 deletions
diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc index fd757b39..27103bd0 100644 --- a/Dafny/Translator.ssc +++ b/Dafny/Translator.ssc @@ -2047,25 +2047,58 @@ namespace Microsoft.Dafny { // use simple heuristics to create a default decreases clause, if none is given
List<Expression!> theDecreases = s.Decreases;
- if (theDecreases.Count == 0) {
- Expression guess = null;
- BinaryExpr bin = s.Guard as BinaryExpr;
- if (bin != null) {
- switch (bin.ResolvedOp) {
- case BinaryExpr.ResolvedOpcode.Lt:
- case BinaryExpr.ResolvedOpcode.Le:
- guess = IntSub(s.Tok, bin.E1, bin.E0);
- break;
- case BinaryExpr.ResolvedOpcode.Ge:
- case BinaryExpr.ResolvedOpcode.Gt:
- guess = IntSub(s.Tok, bin.E0, bin.E1);
- break;
- default:
- break;
+ bool inferredDecreases = false;
+ if (theDecreases.Count == 0 && s.Guard != null) {
+ Expression prefix = null;
+ foreach (Expression guardConjunct in Conjuncts(s.Guard)) {
+ Expression guess = null;
+ BinaryExpr bin = guardConjunct as BinaryExpr;
+ if (bin != null) {
+ switch (bin.ResolvedOp) {
+ case BinaryExpr.ResolvedOpcode.Lt:
+ case BinaryExpr.ResolvedOpcode.Le:
+ // for A < B and A <= B, use the decreases B - A
+ guess = CreateIntSub(s.Tok, bin.E1, bin.E0);
+ break;
+ case BinaryExpr.ResolvedOpcode.Ge:
+ case BinaryExpr.ResolvedOpcode.Gt:
+ // for A >= B and A > B, use the decreases A - B
+ guess = CreateIntSub(s.Tok, bin.E0, bin.E1);
+ break;
+ case BinaryExpr.ResolvedOpcode.NeqCommon:
+ if (bin.E0.Type is IntType) {
+ // for A != B where A and B are integers, use the absolute difference between A and B (that is: if 0 <= A-B then A-B else B-A)
+ Expression AminusB = CreateIntSub(s.Tok, bin.E0, bin.E1);
+ Expression BminusA = CreateIntSub(s.Tok, bin.E1, bin.E0);
+ Expression zero = CreateIntLiteral(s.Tok, 0);
+ BinaryExpr test = new BinaryExpr(s.Tok, BinaryExpr.Opcode.Le, zero, AminusB);
+ test.ResolvedOp = BinaryExpr.ResolvedOpcode.Le; // resolve here
+ test.Type = Type.Bool; // resolve here
+ guess = CreateIntITE(s.Tok, test, AminusB, BminusA);
+ }
+ break;
+ default:
+ break;
+ }
+ }
+ if (guess != null) {
+ if (prefix != null) {
+ // Make the following guess: if prefix then guess else -1
+ Expression negativeOne = CreateIntLiteral(s.Tok, -1);
+ guess = CreateIntITE(s.Tok, prefix, guess, negativeOne);
+ }
+ theDecreases.Add(guess);
+ inferredDecreases = true;
+ break; // ignore any further conjuncts
+ }
+ if (prefix == null) {
+ prefix = guardConjunct;
+ } else {
+ BinaryExpr and = new BinaryExpr(s.Tok, BinaryExpr.Opcode.And, prefix, guardConjunct);
+ and.ResolvedOp = BinaryExpr.ResolvedOpcode.And; // resolve here
+ and.Type = Type.Bool; // resolve here
+ prefix = and;
}
- }
- if (guess != null) {
- theDecreases.Add(guess);
}
}
@@ -2189,7 +2222,7 @@ namespace Microsoft.Dafny { decrs.Add(etran.TrExpr(e));
}
Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrs, oldBfs, loopBodyBuilder, etran, " at end of loop iteration");
- loopBodyBuilder.Add(Assert(stmt.Tok, decrCheck, "decreases expression might not decrease"));
+ loopBodyBuilder.Add(Assert(stmt.Tok, decrCheck, inferredDecreases ? "cannot prove termination; try supplying a decreases clause for the loop" : "decreases expression might not decrease"));
}
Bpl.StmtList body = loopBodyBuilder.Collect(stmt.Tok);
@@ -2368,15 +2401,53 @@ namespace Microsoft.Dafny { }
}
- static Expression! IntSub(Token! tok, Expression! e0, Expression! e1)
+ static Expression! CreateIntLiteral(Token! tok, int n)
+ {
+ if (0 <= n) {
+ Expression lit = new LiteralExpr(tok, n);
+ lit.Type = Type.Int; // resolve here
+ return lit;
+ } else {
+ return CreateIntSub(tok, CreateIntLiteral(tok, 0), CreateIntLiteral(tok, -n));
+ }
+ }
+
+ static Expression! CreateIntSub(Token! tok, Expression! e0, Expression! e1)
requires e0.Type is IntType && e1.Type is IntType;
{
BinaryExpr s = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, e0, e1);
- s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;
- s.Type = Type.Int;
+ s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub; // resolve here
+ s.Type = Type.Int; // resolve here
return s;
}
+ static Expression! CreateIntITE(Token! tok, Expression! test, Expression! e0, Expression! e1)
+ requires test.Type is BoolType && e0.Type is IntType && e1.Type is IntType;
+ {
+ ITEExpr ite = new ITEExpr(tok, test, e0, e1);
+ ite.Type = Type.Int; // resolve here
+ return ite;
+ }
+
+ public IEnumerable<Expression!>! Conjuncts(Expression! expr)
+ requires expr.Type is BoolType;
+ {
+ if (expr is BinaryExpr) {
+ BinaryExpr bin = (BinaryExpr)expr;
+ if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {
+ foreach (Expression e in Conjuncts(bin.E0)) {
+ yield return e;
+ }
+ assert bin != null; // the necessity of this cast is a compiler bug, but perhaps an irrepairable one
+ foreach (Expression e in Conjuncts(bin.E1)) {
+ yield return e;
+ }
+ yield break;
+ }
+ }
+ yield return expr;
+ }
+
void CheckCallTermination(Token! tok, List<Expression!>! contextDecreases, List<Expression!>! calleeDecreases,
Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap,
ExpressionTranslator! etran, Bpl.StmtListBuilder! builder)
diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy index 1ab76a78..cd4a18c2 100644 --- a/Test/VSI-Benchmarks/b1.dfy +++ b/Test/VSI-Benchmarks/b1.dfy @@ -1,75 +1,71 @@ -// Note: To prove termination of calls, methods need
-// a termination measure, but Dafny does not yet support
-// termination measures for methods (but it will in
-// the foreseeable future).
-
// Spec# and Boogie and Chalice: The program will be
// the same, except that these languages do not check
-// for any kind of termination.
+// for any kind of termination. Also, in Spec#, there
+// is an issue of potential overflows.
+
+// Benchmark1
-class Benchmark1 {
- method Add(x: int, y: int) returns (r: int)
- ensures r == x+y;
- {
- r := x;
- if (y < 0) {
- var n := y;
- while (n != 0)
- invariant r == x+y-n && 0 <= -n;
- decreases -n;
- {
- r := r - 1;
- n := n + 1;
- }
- } else {
- var n := y;
- while (n != 0)
- invariant r == x+y-n && 0 <= n;
- decreases n;
- {
- r := r + 1;
- n := n - 1;
- }
+method Add(x: int, y: int) returns (r: int)
+ ensures r == x+y;
+{
+ r := x;
+ if (y < 0) {
+ var n := y;
+ while (n != 0)
+ invariant r == x+y-n && 0 <= -n;
+ {
+ r := r - 1;
+ n := n + 1;
+ }
+ } else {
+ var n := y;
+ while (n != 0)
+ invariant r == x+y-n && 0 <= n;
+ {
+ r := r + 1;
+ n := n - 1;
}
}
+}
- method Mul(x: int, y: int) returns (r: int)
- ensures r == x*y;
- decreases x < 0, x;
- {
- if (x == 0) {
- r := 0;
- } else if (x < 0) {
- call r := Mul(-x, y);
- r := -r;
- } else {
- call r := Mul(x-1, y);
- call r := Add(r, y);
- }
+method Mul(x: int, y: int) returns (r: int)
+ ensures r == x*y;
+ decreases x < 0, x;
+{
+ if (x == 0) {
+ r := 0;
+ } else if (x < 0) {
+ call r := Mul(-x, y);
+ r := -r;
+ } else {
+ call r := Mul(x-1, y);
+ call r := Add(r, y);
}
+}
- method Main() {
- call TestAdd(3, 180);
- call TestAdd(3, -180);
- call TestAdd(0, 1);
+// ---------------------------
- call TestMul(3, 180);
- call TestMul(3, -180);
- call TestMul(180, 3);
- call TestMul(-180, 3);
- call TestMul(0, 1);
- call TestMul(1, 0);
- }
+method Main() {
+ call TestAdd(3, 180);
+ call TestAdd(3, -180);
+ call TestAdd(0, 1);
- method TestAdd(x: int, y: int) {
- print x, " + ", y, " = ";
- call z := Add(x, y);
- print z, "\n";
- }
+ call TestMul(3, 180);
+ call TestMul(3, -180);
+ call TestMul(180, 3);
+ call TestMul(-180, 3);
+ call TestMul(0, 1);
+ call TestMul(1, 0);
+}
- method TestMul(x: int, y: int) {
- print x, " * ", y, " = ";
- call z := Mul(x, y);
- print z, "\n";
- }
+method TestAdd(x: int, y: int) {
+ print x, " + ", y, " = ";
+ call z := Add(x, y);
+ print z, "\n";
+}
+
+method TestMul(x: int, y: int) {
+ print x, " * ", y, " = ";
+ call z := Mul(x, y);
+ print z, "\n";
}
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy index fd20a72b..1021ee85 100644 --- a/Test/VSI-Benchmarks/b2.dfy +++ b/Test/VSI-Benchmarks/b2.dfy @@ -14,7 +14,6 @@ class Benchmark2 { invariant 0 <= low && low <= high && high <= |a|;
invariant (forall i :: 0 <= i && i < low ==> a[i] < key);
invariant (forall i :: high <= i && i < |a| ==> key < a[i]);
- decreases high - low;
{
var mid := low + (high - low) / 2;
var midVal := a[mid];
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 6d9c3ddd..d9acfe04 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -88,8 +88,6 @@ class Benchmark3 { // the current array is that permutation of the input array
invariant (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
invariant (forall i: int :: 0 <= i && i < |p| ==> q.contents[i] == old(q.contents)[p[i]]);
-
- decreases |q.contents|;
{
call m,k := RemoveMin(q);
perm := perm + [p[k]]; //adds index of min to perm
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index 34e0cfef..a37f86e4 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -78,14 +78,13 @@ class Glossary { var wr := new WriterStream;
call wr.Create();
- while (0<|q.contents|)
+ while (0 < |q.contents|)
invariant wr.Valid() && fresh(wr.footprint);
invariant glossary.Valid();
invariant glossary !in wr.footprint && null !in glossary.keys;
invariant (forall d :: d in glossary.values ==> null !in d);
invariant q !in wr.footprint;
invariant (forall k :: k in q.contents ==> k in glossary.keys);
- decreases |q.contents|;
{
call term := q.Dequeue();
call present,definition := glossary.Find(term);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index cc248c20..7456ffaa 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -101,26 +101,26 @@ Execution trace: SmallTests.dfy(81,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-SmallTests.dfy(95,5): Error: call may violate caller's modifies clause
+SmallTests.dfy(116,5): Error: call may violate caller's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
(0,0): anon3
-SmallTests.dfy(108,7): Error: call may violate caller's modifies clause
+SmallTests.dfy(129,7): Error: call may violate caller's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-SmallTests.dfy(110,7): Error: call may violate caller's modifies clause
+SmallTests.dfy(131,7): Error: call may violate caller's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-SmallTests.dfy(150,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
+SmallTests.dfy(171,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
(0,0): anon3
-Dafny program verifier finished with 24 verified, 9 errors
+Dafny program verifier finished with 28 verified, 9 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
@@ -226,7 +226,7 @@ Execution trace: (0,0): anon16_LoopBody
Definedness.dfy(151,5): anon17_Else
(0,0): anon9
-Definedness.dfy(172,44): Error: loop invariant must be well defined
+Definedness.dfy(170,44): Error: loop invariant must be well defined
Execution trace:
(0,0): anon0
Definedness.dfy(162,5): anon16_LoopHead
@@ -235,28 +235,28 @@ Execution trace: (0,0): anon3
(0,0): anon18_Then
(0,0): anon6
- Definedness.dfy(170,5): anon19_LoopHead
+ Definedness.dfy(169,5): anon19_LoopHead
(0,0): anon19_LoopBody
(0,0): anon20_Then
-Definedness.dfy(193,21): Error: collection expression must be well defined
+Definedness.dfy(191,21): Error: collection expression must be well defined
Execution trace:
(0,0): anon0
-Definedness.dfy(195,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
+Definedness.dfy(193,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
Execution trace:
(0,0): anon0
-Definedness.dfy(197,33): Error: range expression must be well defined
+Definedness.dfy(195,33): Error: range expression must be well defined
Execution trace:
(0,0): anon0
-Definedness.dfy(203,18): Error: RHS of assignment must be well defined
+Definedness.dfy(201,18): Error: RHS of assignment must be well defined
Execution trace:
(0,0): anon0
-Definedness.dfy(212,23): Error: loop invariant must be well defined
+Definedness.dfy(210,23): Error: loop invariant must be well defined
Execution trace:
(0,0): anon0
- Definedness.dfy(210,5): anon7_LoopHead
+ Definedness.dfy(208,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-Definedness.dfy(212,23): Error BP5004: This loop invariant might not hold on entry.
+Definedness.dfy(210,23): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
@@ -335,8 +335,44 @@ Execution trace: Dafny program verifier finished with 2 verified, 1 error
-------------------- Termination.dfy --------------------
+Termination.dfy(102,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+Execution trace:
+ (0,0): anon0
+ Termination.dfy(102,3): anon7_LoopHead
+ (0,0): anon7_LoopBody
+ Termination.dfy(102,3): anon8_Else
+ (0,0): anon3
+ Termination.dfy(102,12): anon9_Else
+ (0,0): anon5
+Termination.dfy(110,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+Execution trace:
+ (0,0): anon0
+ Termination.dfy(110,3): anon7_LoopHead
+ (0,0): anon7_LoopBody
+ Termination.dfy(110,3): anon8_Else
+ (0,0): anon3
+ Termination.dfy(110,16): anon9_Else
+ (0,0): anon5
+Termination.dfy(119,3): Error: decreases expression might not decrease
+Execution trace:
+ (0,0): anon0
+ Termination.dfy(119,3): anon7_LoopHead
+ (0,0): anon7_LoopBody
+ Termination.dfy(119,3): anon8_Else
+ (0,0): anon3
+ Termination.dfy(119,16): anon9_Else
+ (0,0): anon5
+Termination.dfy(120,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
+Execution trace:
+ (0,0): anon0
+ Termination.dfy(119,3): anon7_LoopHead
+ (0,0): anon7_LoopBody
+ Termination.dfy(119,3): anon8_Else
+ (0,0): anon3
+ Termination.dfy(119,16): anon9_Else
+ (0,0): anon5
-Dafny program verifier finished with 13 verified, 0 errors
+Dafny program verifier finished with 22 verified, 4 errors
-------------------- Use.dfy --------------------
Use.dfy(16,18): Error: assertion violation
@@ -363,7 +399,7 @@ Execution trace: Use.dfy(138,5): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(209,19): Error: assertion violation
+Use.dfy(208,19): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy index b69fa4f6..d557de21 100644 --- a/Test/dafny0/Definedness.dfy +++ b/Test/dafny0/Definedness.dfy @@ -161,14 +161,12 @@ class StatementTwoShoes { var i := 0;
while (i < 100)
invariant i <= 100;
- decreases 100 - i;
invariant F(123 - i) == this;
{
i := i + 1;
}
i := 0;
while (i < 100)
- decreases 100 - i;
invariant F(if i==77 then -3 else i) == this; // error: expression may not be well defined
{
i := i + 1;
@@ -210,7 +208,6 @@ class StatementTwoShoes { while (i < 100)
// The following line produces two complaints, thanks to the w-encoding of the loop's invariant definedness checking
invariant 5 / x != 5 / x; // error: not well-defined, and error: loop invariant does not hold initially
- decreases 100 - i;
{
i := i + 1;
}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 4e3fab69..87bfd35f 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -85,6 +85,27 @@ class Modifies { }
}
+ method Aprime(p: Modifies)
+ modifies this, p;
+ {
+ x := x + 1;
+ while (p != null && p.x < 75)
+ decreases if p != null then 75 - p.x else 0; // given explicitly (but see Adoubleprime below)
+ {
+ p.x := p.x + 1;
+ }
+ }
+
+ method Adoubleprime(p: Modifies)
+ modifies this, p;
+ {
+ x := x + 1;
+ while (p != null && p.x < 75) // here, the decreases clause is heuristically inferred (to be the
+ { // same as the one in Aprime above)
+ p.x := p.x + 1;
+ }
+ }
+
method B(p: Modifies)
modifies this;
{
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index 39361b7b..27004653 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -5,7 +5,7 @@ class Termination { var i := 0;
while (i < N)
invariant i <= N;
- decreases N - i;
+ // this will be heuristically inferred: decreases N - i;
{
i := i + 1;
}
@@ -95,3 +95,59 @@ datatype List<T> { Nil;
Cons(T, List<T>);
}
+
+method FailureToProveTermination0(N: int)
+{
+ var n := N;
+ while (n < 100) { // error: may not terminate
+ n := n - 1;
+ }
+}
+
+method FailureToProveTermination1(x: int, y: int, N: int)
+{
+ var n := N;
+ while (x < y && n < 100) // error: cannot prove termination from the heuristically chosen termination metric
+ {
+ n := n + 1;
+ }
+}
+
+method FailureToProveTermination2(x: int, y: int, N: int)
+{
+ var n := N;
+ while (x < y && n < 100) // error: cannot prove termination from the given (bad) termination metric
+ decreases n - x;
+ {
+ n := n + 1;
+ }
+}
+
+method FailureToProveTermination3(x: int, y: int, N: int)
+{
+ var n := N;
+ while (x < y && n < 100)
+ decreases 100 - n;
+ {
+ n := n + 1;
+ }
+}
+
+method FailureToProveTermination4(x: int, y: int, N: int)
+{
+ var n := N;
+ while (n < 100 && x < y)
+ decreases 100 - n;
+ {
+ n := n + 1;
+ }
+}
+
+method FailureToProveTermination5(b: bool, N: int)
+{
+ var n := N;
+ while (b && n < 100) // here, the heuristics are good enough to prove termination
+ {
+ n := n + 1;
+ }
+}
diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy index aaf41190..20928f41 100644 --- a/Test/dafny0/Use.dfy +++ b/Test/dafny0/Use.dfy @@ -191,7 +191,6 @@ class Recursive { while (k < n)
invariant k <= n;
invariant Gauss(k) == (k+1)*k / 2;
- decreases n - k;
{
k := k + 1;
}
diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy index a46e83a3..3e64a4bd 100644 --- a/Test/dafny1/SchorrWaite.dfy +++ b/Test/dafny1/SchorrWaite.dfy @@ -64,7 +64,6 @@ class Main { invariant (forall n :: n in S ==>
n.childrenVisited == old(n.childrenVisited) &&
n.children == old(n.children));
- decreases |root.children| - i;
{
var c := root.children[i];
if (c != null) {
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy index 72415fea..9e4da459 100644 --- a/Test/dafny1/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy @@ -96,7 +96,6 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int) while (j < N)
invariant j <= N;
invariant (forall k :: 0 <= k && k < j ==> seArgs2[k] == seArgs[k]);
- decreases N - j;
{
call TheoremSeq(args[j], v, val);
j := j + 1;
diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy index da1f63bb..0e6aff05 100644 --- a/Test/vacid0/SparseArray.dfy +++ b/Test/vacid0/SparseArray.dfy @@ -55,7 +55,6 @@ class SparseArray<T> { // TODO: why doesn't this work instead of the next line? invariant (forall x :: x in s ==> x == zero);
invariant (forall i :: 0 <= i && i < |s| ==> s[i] == zero);
invariant |id| == k && (forall i :: 0 <= i && i < k ==> id[i] == i);
- decreases N - k;
{
s := s + [zero];
id := id + [k];
@@ -110,7 +109,6 @@ class SparseArray<T> { var i := 0;
while (i < n)
invariant i <= n && |arr| == i;
- decreases n - i;
{
var g: G;
arr := arr + [g];
|