diff options
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 136 | ||||
| -rw-r--r-- | Test/dafny0/BinaryTree.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny0/Definedness.dfy | 218 | ||||
| -rw-r--r-- | Test/dafny0/Modules0.dfy | 34 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 219 | ||||
| -rw-r--r-- | Test/dafny0/SumOfCubes.dfy | 20 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 3 |
7 files changed, 338 insertions, 294 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 3186ae01..5dadda4b 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -12,23 +12,23 @@ class MyClass<T, U> { ensures t == t;
ensures old(null) != this;
{
- x := 12;
- while (x < 100)
- invariant x <= 100;
- {
- x := x + 17;
- if (x % 20 == 3) {
- x := this.x + 1;
- } else {
- this.x := x + 0;
+ x := 12;
+ while (x < 100)
+ invariant x <= 100;
+ {
+ x := x + 17;
+ if (x % 20 == 3) {
+ x := this.x + 1;
+ } else {
+ this.x := x + 0;
+ }
+ call t, u, v := M(true, lotsaObjects)
+ var to: MyClass<T,U>;
+ call to, u, v := M(true, lotsaObjects)
+ call to, u, v := to.M(true, lotsaObjects)
+ assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
}
- call t, u, v := M(true, lotsaObjects)
- var to: MyClass<T,U>;
- call to, u, v := M(true, lotsaObjects)
- call to, u, v := to.M(true, lotsaObjects)
- assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
}
- }
function F(x: int, y: int, h: WildData, k: WildData): WildData
{
@@ -122,144 +122,154 @@ Execution trace: (0,0): anon0
(0,0): anon4_Else
(0,0): anon3
-SmallTests.dfy(162,7): Error: possible division by zero
+
+Dafny program verifier finished with 22 verified, 9 errors
+
+-------------------- Definedness.dfy --------------------
+Definedness.dfy(8,7): Error: possible division by zero
Execution trace:
(0,0): anon0
-SmallTests.dfy(169,16): Error: possible division by zero
+Definedness.dfy(15,16): Error: possible division by zero
Execution trace:
(0,0): anon0
-SmallTests.dfy(178,16): Error: target object may be null
+Definedness.dfy(24,16): Error: target object may be null
Execution trace:
(0,0): anon0
-SmallTests.dfy(179,21): Error: target object may be null
+Definedness.dfy(25,21): Error: target object may be null
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-SmallTests.dfy(180,17): Error: possible division by zero
+Definedness.dfy(26,17): Error: possible division by zero
Execution trace:
(0,0): anon0
-SmallTests.dfy(187,16): Error: target object may be null
+Definedness.dfy(33,16): Error: target object may be null
Execution trace:
(0,0): anon0
-SmallTests.dfy(204,18): Error: target object may be null
+Definedness.dfy(50,18): Error: target object may be null
Execution trace:
(0,0): anon0
-SmallTests.dfy(209,18): Error: target object may be null
+Definedness.dfy(55,18): Error: target object may be null
Execution trace:
(0,0): anon0
-SmallTests.dfy(231,9): Error: LHS expression must be well defined
+Definedness.dfy(77,9): Error: LHS expression must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(232,12): Error: LHS expression must be well defined
+Definedness.dfy(78,12): Error: LHS expression must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(233,7): Error: RHS expression must be well defined
+Definedness.dfy(79,7): Error: RHS expression must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(238,18): Error: assert condition must be well defined
+Definedness.dfy(84,18): Error: assert condition must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(239,5): Error: assume condition must be well defined
+Definedness.dfy(85,5): Error: assume condition must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(244,16): Error: if guard must be well defined
+Definedness.dfy(90,16): Error: if guard must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(251,19): Error: loop guard must be well defined
+Definedness.dfy(97,19): Error: loop guard must be well defined
Execution trace:
(0,0): anon0
- SmallTests.dfy(251,5): anon8_LoopHead
+ Definedness.dfy(97,5): anon8_LoopHead
(0,0): anon8_LoopBody
- SmallTests.dfy(251,5): anon9_Else
+ Definedness.dfy(97,5): anon9_Else
(0,0): anon3
-SmallTests.dfy(260,23): Error: decreases expression must be well defined at top of each loop iteration
+Definedness.dfy(106,23): Error: decreases expression must be well defined at top of each loop iteration
Execution trace:
(0,0): anon0
- SmallTests.dfy(259,5): anon13_LoopHead
+ Definedness.dfy(105,5): anon13_LoopHead
(0,0): anon13_LoopBody
(0,0): anon14_Then
-SmallTests.dfy(266,17): Error: decreases expression must be well defined at top of each loop iteration
+Definedness.dfy(112,17): Error: decreases expression must be well defined at top of each loop iteration
Execution trace:
(0,0): anon0
- SmallTests.dfy(259,5): anon13_LoopHead
+ Definedness.dfy(105,5): anon13_LoopHead
(0,0): anon13_LoopBody
- SmallTests.dfy(259,5): anon14_Else
+ Definedness.dfy(105,5): anon14_Else
(0,0): anon3
(0,0): anon15_Then
(0,0): anon6
- SmallTests.dfy(265,5): anon16_LoopHead
+ Definedness.dfy(111,5): anon16_LoopHead
(0,0): anon16_LoopBody
(0,0): anon17_Then
-SmallTests.dfy(276,22): Error: loop invariant must be well defined
+Definedness.dfy(122,22): Error: loop invariant must be well defined
Execution trace:
(0,0): anon0
- SmallTests.dfy(275,5): anon7_LoopHead
+ Definedness.dfy(121,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-SmallTests.dfy(276,22): Error BP5004: This loop invariant might not hold on entry.
+Definedness.dfy(122,22): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
-SmallTests.dfy(277,17): Error: decreases expression must be well defined at top of each loop iteration
+Definedness.dfy(123,17): Error: decreases expression must be well defined at top of each loop iteration
Execution trace:
(0,0): anon0
- SmallTests.dfy(275,5): anon7_LoopHead
+ Definedness.dfy(121,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-SmallTests.dfy(286,24): Error: loop guard must be well defined
+Definedness.dfy(132,24): Error: loop guard must be well defined
Execution trace:
(0,0): anon0
- SmallTests.dfy(286,5): anon7_LoopHead
+ Definedness.dfy(132,5): anon7_LoopHead
(0,0): anon7_LoopBody
- SmallTests.dfy(286,5): anon8_Else
+ Definedness.dfy(132,5): anon8_Else
(0,0): anon3
-SmallTests.dfy(305,24): Error: loop guard must be well defined
+Definedness.dfy(151,24): Error: loop guard must be well defined
Execution trace:
(0,0): anon0
- SmallTests.dfy(299,5): anon13_LoopHead
+ Definedness.dfy(145,5): anon13_LoopHead
(0,0): anon13_LoopBody
- SmallTests.dfy(299,5): anon14_Else
+ Definedness.dfy(145,5): anon14_Else
(0,0): anon3
(0,0): anon15_Then
(0,0): anon6
- SmallTests.dfy(305,5): anon16_LoopHead
+ Definedness.dfy(151,5): anon16_LoopHead
(0,0): anon16_LoopBody
- SmallTests.dfy(305,5): anon17_Else
+ Definedness.dfy(151,5): anon17_Else
(0,0): anon9
-SmallTests.dfy(326,44): Error: loop invariant must be well defined
+Definedness.dfy(172,44): Error: loop invariant must be well defined
Execution trace:
(0,0): anon0
- SmallTests.dfy(316,5): anon16_LoopHead
+ Definedness.dfy(162,5): anon16_LoopHead
(0,0): anon16_LoopBody
- SmallTests.dfy(316,5): anon17_Else
+ Definedness.dfy(162,5): anon17_Else
(0,0): anon3
(0,0): anon18_Then
(0,0): anon6
- SmallTests.dfy(324,5): anon19_LoopHead
+ Definedness.dfy(170,5): anon19_LoopHead
(0,0): anon19_LoopBody
(0,0): anon20_Then
-SmallTests.dfy(347,21): Error: collection expression must be well defined
+Definedness.dfy(193,21): Error: collection expression must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(349,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
+Definedness.dfy(195,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
Execution trace:
(0,0): anon0
-SmallTests.dfy(351,33): Error: range expression must be well defined
+Definedness.dfy(197,33): Error: range expression must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(357,18): Error: RHS of assignment must be well defined
+Definedness.dfy(203,18): Error: RHS of assignment must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(366,23): Error: loop invariant must be well defined
+Definedness.dfy(212,23): Error: loop invariant must be well defined
Execution trace:
(0,0): anon0
- SmallTests.dfy(364,5): anon7_LoopHead
+ Definedness.dfy(210,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-SmallTests.dfy(366,23): Error BP5004: This loop invariant might not hold on entry.
+Definedness.dfy(212,23): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 43 verified, 38 errors
+Dafny program verifier finished with 21 verified, 29 errors
+
+-------------------- Modules0.dfy --------------------
+Modules0.dfy(13,7): Error: module T named among imports does not exist
+Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G
+Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
+3 resolution/type errors detected in Modules0.dfy
-------------------- Queue.dfy --------------------
diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy index 5f56cf40..276b6c0e 100644 --- a/Test/dafny0/BinaryTree.dfy +++ b/Test/dafny0/BinaryTree.dfy @@ -48,7 +48,7 @@ class IntSet { footprint := root.footprint + {this};
}
- class method InsertHelper(x: int, n: Node) returns (m: Node)
+ static method InsertHelper(x: int, n: Node) returns (m: Node)
requires n == null || n.Valid();
modifies n.footprint;
ensures m != null && m.Valid();
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy new file mode 100644 index 00000000..4bf6ae30 --- /dev/null +++ b/Test/dafny0/Definedness.dfy @@ -0,0 +1,218 @@ +// ----------------- wellformed specifications ----------------------
+
+class SoWellformed {
+ var xyz: int;
+ var next: SoWellformed;
+
+ function F(x: int): int
+ { 5 / x } // error: possible division by zero
+
+ function G(x: int): int
+ requires 0 < x;
+ { 5 / x }
+
+ function H(x: int): int
+ decreases 5/x; // error: possible division by zero
+ { 12 }
+
+ function I(x: int): int
+ requires 0 < x;
+ decreases 5/x;
+ { 12 }
+
+ method M(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)
+ requires a.xyz == 7; // error: not always defined
+ ensures c ==> d.xyz == -7; // error: not always defined
+ decreases 5 / b; // error: not always defined
+ {
+ c := false;
+ }
+
+ method N(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)
+ decreases 5 / b;
+ requires a.next != null; // error: not always defined
+ requires a.next.xyz == 7; // this is well-defined, given that the previous line is
+ requires b < -2;
+ ensures 0 <= b ==> d.xyz == -7 && !c;
+ {
+ c := true;
+ }
+
+ method O(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)
+ modifies a.next; // this may not be well-defined, but that's okay for modifies clauses
+ {
+ c := true;
+ }
+
+ method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed);
+ requires next != null;
+ modifies this;
+ ensures next.xyz < 100; // error: may not be well-defined (if body sets next to null)
+
+ method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);
+ requires next != null;
+ modifies s;
+ ensures next.xyz < 100; // error: may not be well-defined (if this in s and body sets next to null)
+
+ method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);
+ requires next != null && this !in s;
+ modifies s;
+ ensures next.xyz < 100; // fine
+}
+
+// ---------------------- welldefinedness checks for statements -------------------
+
+class StatementTwoShoes {
+ var x: int;
+
+ function method F(b: int): StatementTwoShoes
+ requires 0 <= b;
+ {
+ this
+ }
+
+ method M(p: StatementTwoShoes, a: int)
+ modifies this, p;
+ {
+ p.x := a; // error: receiver may be null
+ F(a).x := a; // error: LHS may not be well defined
+ x := F(a-10).x; // error: RHS may not be well defined
+ }
+
+ method N(a: int, b: int)
+ {
+ assert 5 / a == 5 / a; // error: expression may not be well defined
+ assume 20 / b == 5; // error: expression may not be well defined
+ }
+
+ method O(a: int) returns (b: int)
+ {
+ if (20 / a == 5) { // error: expression may not be well defined
+ b := a;
+ }
+ }
+
+ method P(a: int)
+ {
+ while (20 / a == 5) { // error: expression may not be well defined
+ break;
+ }
+ }
+
+ method Q(a: int, b: int)
+ {
+ var i := 1;
+ while (i < a)
+ decreases F(i), F(a), a - i; // error: component 1 may not be well defined
+ {
+ i := i + 1;
+ }
+ i := 1;
+ while (i < a)
+ decreases F(b), a - i; // error: component 0 may not be well defined
+ {
+ i := i + 1;
+ }
+ }
+
+ method R(a: int)
+ {
+ var i := 0;
+ while (i < 100) // The following produces 3 complaints instead of 1, because loop invariants are not subject to subsumption
+ invariant F(a) != null; // error: expression may not be well defined, and error: loop invariant may not hold
+ decreases F(a), 100 - i; // error: component 0 not well defined
+ {
+ i := i + 1;
+ }
+ }
+
+ method S(a: int)
+ {
+ var j := 0;
+ while (20 / a == 5 && j < 100) // error: guard may not be well defined
+ invariant j <= 100;
+ decreases F(101 - j), 100 - j;
+ {
+ j := j + 1;
+ }
+ }
+
+ method T(a: int)
+ requires a != 0 && 20 / a == 5;
+ {
+ var k := a;
+ var j := 0;
+ while (20 / k == 5 && j < 100) // fine
+ decreases 100 - j;
+ {
+ j := j + 1;
+ }
+ j := 0;
+ while (20 / k == 5 && j < 100) // error: guard may not be well defined
+ decreases 100 - j;
+ {
+ havoc k;
+ j := j + 1;
+ }
+ }
+
+ method U()
+ {
+ 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;
+ if (i == 77) { i := i + 1; }
+ }
+ }
+
+ use function G(w: int): int { 5 }
+ function method H(x: int): int;
+
+ method V(s: set<StatementTwoShoes>, a: int, b: int)
+ modifies s;
+ {
+ use G(12 / b); // fine, because there are no welldefinedness checks on use statements
+ foreach (m in s | m.x < 200) // s may contain null, but the foreach excludes null
+ {
+ assume 0 <= m.x;
+ assert m.x < 1000;
+ use G(5 / m.x); // fine, because there are no welldefinedness checks on use statements
+ m.x := m.x + 1;
+ }
+ foreach (m in s + {F(a)}) // error: collection expression may not be well defined
+ {
+ m.x := 5; // error: possible modifies clause violation
+ }
+ foreach (m in s | F(H(m.x)) == this) // error: range expression may not be well defined
+ {
+ m.x := H(m.x);
+ }
+ foreach (m in s)
+ {
+ m.x := 100 / m.x; // error: RhS may not be well defined
+ }
+ }
+
+ method W(x: int)
+ {
+ var i := 0;
+ 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/Modules0.dfy b/Test/dafny0/Modules0.dfy new file mode 100644 index 00000000..cf616fba --- /dev/null +++ b/Test/dafny0/Modules0.dfy @@ -0,0 +1,34 @@ +module M {
+ class T { }
+ class U { }
+}
+
+module N {
+ class T { } // error: duplicate class name
+}
+
+module U imports N { // fine, despite the fact that a class is called U--module names are in their own name space
+}
+
+module V imports T { // error: T is not a module
+}
+
+module A imports B, M {
+ class Y { }
+}
+
+module B imports N, M {
+ class X { }
+}
+
+module G imports A, M, A, H, B { // error: cycle in import graph
+}
+
+module H imports A, N, I {
+}
+
+module I imports J {
+}
+
+module J imports G, M {
+}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 3bf5ed3f..b627df75 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -151,222 +151,3 @@ class Modifies { }
}
}
-
-// ----------------- wellformed specifications ----------------------
-
-class SoWellformed {
- var xyz: int;
- var next: SoWellformed;
-
- function F(x: int): int
- { 5 / x } // error: possible division by zero
-
- function G(x: int): int
- requires 0 < x;
- { 5 / x }
-
- function H(x: int): int
- decreases 5/x; // error: possible division by zero
- { 12 }
-
- function I(x: int): int
- requires 0 < x;
- decreases 5/x;
- { 12 }
-
- method M(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)
- requires a.xyz == 7; // error: not always defined
- ensures c ==> d.xyz == -7; // error: not always defined
- decreases 5 / b; // error: not always defined
- {
- c := false;
- }
-
- method N(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)
- decreases 5 / b;
- requires a.next != null; // error: not always defined
- requires a.next.xyz == 7; // this is well-defined, given that the previous line is
- requires b < -2;
- ensures 0 <= b ==> d.xyz == -7 && !c;
- {
- c := true;
- }
-
- method O(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)
- modifies a.next; // this may not be well-defined, but that's okay for modifies clauses
- {
- c := true;
- }
-
- method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed);
- requires next != null;
- modifies this;
- ensures next.xyz < 100; // error: may not be well-defined (if body sets next to null)
-
- method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);
- requires next != null;
- modifies s;
- ensures next.xyz < 100; // error: may not be well-defined (if this in s and body sets next to null)
-
- method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);
- requires next != null && this !in s;
- modifies s;
- ensures next.xyz < 100; // fine
-}
-
-// ---------------------- welldefinedness checks for statements -------------------
-
-class StatementTwoShoes {
- var x: int;
-
- function method F(b: int): StatementTwoShoes
- requires 0 <= b;
- {
- this
- }
-
- method M(p: StatementTwoShoes, a: int)
- modifies this, p;
- {
- p.x := a; // error: receiver may be null
- F(a).x := a; // error: LHS may not be well defined
- x := F(a-10).x; // error: RHS may not be well defined
- }
-
- method N(a: int, b: int)
- {
- assert 5 / a == 5 / a; // error: expression may not be well defined
- assume 20 / b == 5; // error: expression may not be well defined
- }
-
- method O(a: int) returns (b: int)
- {
- if (20 / a == 5) { // error: expression may not be well defined
- b := a;
- }
- }
-
- method P(a: int)
- {
- while (20 / a == 5) { // error: expression may not be well defined
- break;
- }
- }
-
- method Q(a: int, b: int)
- {
- var i := 1;
- while (i < a)
- decreases F(i), F(a), a - i; // error: component 1 may not be well defined
- {
- i := i + 1;
- }
- i := 1;
- while (i < a)
- decreases F(b), a - i; // error: component 0 may not be well defined
- {
- i := i + 1;
- }
- }
-
- method R(a: int)
- {
- var i := 0;
- while (i < 100) // The following produces 3 complaints instead of 1, because loop invariants are not subject to subsumption
- invariant F(a) != null; // error: expression may not be well defined, and error: loop invariant may not hold
- decreases F(a), 100 - i; // error: component 0 not well defined
- {
- i := i + 1;
- }
- }
-
- method S(a: int)
- {
- var j := 0;
- while (20 / a == 5 && j < 100) // error: guard may not be well defined
- invariant j <= 100;
- decreases F(101 - j), 100 - j;
- {
- j := j + 1;
- }
- }
-
- method T(a: int)
- requires a != 0 && 20 / a == 5;
- {
- var k := a;
- var j := 0;
- while (20 / k == 5 && j < 100) // fine
- decreases 100 - j;
- {
- j := j + 1;
- }
- j := 0;
- while (20 / k == 5 && j < 100) // error: guard may not be well defined
- decreases 100 - j;
- {
- havoc k;
- j := j + 1;
- }
- }
-
- method U()
- {
- 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;
- if (i == 77) { i := i + 1; }
- }
- }
-
- use function G(w: int): int { 5 }
- function method H(x: int): int;
-
- method V(s: set<StatementTwoShoes>, a: int, b: int)
- modifies s;
- {
- use G(12 / b); // fine, because there are no welldefinedness checks on use statements
- foreach (m in s | m.x < 200) // s may contain null, but the foreach excludes null
- {
- assume 0 <= m.x;
- assert m.x < 1000;
- use G(5 / m.x); // fine, because there are no welldefinedness checks on use statements
- m.x := m.x + 1;
- }
- foreach (m in s + {F(a)}) // error: collection expression may not be well defined
- {
- m.x := 5; // error: possible modifies clause violation
- }
- foreach (m in s | F(H(m.x)) == this) // error: range expression may not be well defined
- {
- m.x := H(m.x);
- }
- foreach (m in s)
- {
- m.x := 100 / m.x; // error: RhS may not be well defined
- }
- }
-
- method W(x: int)
- {
- var i := 0;
- 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/SumOfCubes.dfy b/Test/dafny0/SumOfCubes.dfy index 389c885c..42a82fe6 100644 --- a/Test/dafny0/SumOfCubes.dfy +++ b/Test/dafny0/SumOfCubes.dfy @@ -1,12 +1,12 @@ class SumOfCubes {
- class use function SumEmUp(n: int, m: int): int
+ static use function SumEmUp(n: int, m: int): int
requires 0 <= n && n <= m;
decreases m - n;
{
if m == n then 0 else n*n*n + SumEmUp(n+1, m)
}
- class method Socu(n: int, m: int) returns (r: int)
+ static method Socu(n: int, m: int) returns (r: int)
requires 0 <= n && n <= m;
ensures r == SumEmUp(n, m);
{
@@ -16,7 +16,7 @@ class SumOfCubes { call Lemma0(n, m);
}
- class method SocuFromZero(k: int) returns (r: int)
+ static method SocuFromZero(k: int) returns (r: int)
requires 0 <= k;
ensures r == SumEmUp(0, k);
{
@@ -25,7 +25,7 @@ class SumOfCubes { call Lemma1(k);
}
- ghost class method Lemma0(n: int, m: int)
+ ghost static method Lemma0(n: int, m: int)
requires 0 <= n && n <= m;
ensures SumEmUp(n, m) == SumEmUp(0, m) - SumEmUp(0, n);
{
@@ -42,14 +42,14 @@ class SumOfCubes { call Lemma3(0, k);
}
- class use function GSum(k: int): int
+ static use function GSum(k: int): int
requires 0 <= k;
decreases k;
{
if k == 0 then 0 else GSum(k-1) + k-1
}
- ghost class method Gauss(k: int) returns (r: int)
+ ghost static method Gauss(k: int) returns (r: int)
requires 0 <= k;
ensures r == GSum(k);
{
@@ -57,7 +57,7 @@ class SumOfCubes { call Lemma2(k);
}
- ghost class method Lemma1(k: int)
+ ghost static method Lemma1(k: int)
requires 0 <= k;
ensures SumEmUp(0, k) == GSum(k) * GSum(k);
{
@@ -73,7 +73,7 @@ class SumOfCubes { call Lemma3(0, k);
}
- ghost class method Lemma2(k: int)
+ ghost static method Lemma2(k: int)
requires 0 <= k;
ensures 2 * GSum(k) == k * (k - 1);
{
@@ -87,14 +87,14 @@ class SumOfCubes { }
}
- class use function SumEmDown(n: int, m: int): int
+ static use function SumEmDown(n: int, m: int): int
requires 0 <= n && n <= m;
decreases m;
{
if m == n then 0 else SumEmDown(n, m-1) + (m-1)*(m-1)*(m-1)
}
- ghost class method Lemma3(n: int, m: int)
+ ghost static method Lemma3(n: int, m: int)
requires 0 <= n && n <= m;
ensures SumEmUp(n, m) == SumEmDown(n, m);
{
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index c1837b43..2bec0a4d 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -17,7 +17,8 @@ for %%f in (BQueue.bpl) do ( %BPLEXE% %* %%f
)
-for %%f in (TypeTests.dfy SmallTests.dfy Queue.dfy ListCopy.dfy
+for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy
+ Modules0.dfy Queue.dfy ListCopy.dfy
BinaryTree.dfy ListReverse.dfy ListContents.dfy
SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy
|