diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny0/Calculations.dfy | 10 |
2 files changed, 8 insertions, 6 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 6e775b43..e31ef49c 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1796,10 +1796,10 @@ Calculations.dfy(8,17): Error: assertion violation Execution trace:
(0,0): anon0
(0,0): anon19_Then
-Calculations.dfy(42,11): Error: assertion violation
+Calculations.dfy(44,11): Error: assertion violation
Execution trace:
(0,0): anon0
- Calculations.dfy(37,2): anon5_Else
+ Calculations.dfy(39,2): anon5_Else
Dafny program verifier finished with 5 verified, 4 errors
diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy index aa447d9f..8ef36139 100644 --- a/Test/dafny0/Calculations.dfy +++ b/Test/dafny0/Calculations.dfy @@ -17,10 +17,12 @@ method CalcTest0(s: seq<int>) { } } assume forall x :: x in s ==> x >= 0; - calc ==> { + calc { 0 < |s|; - { assert s[0] >= 0; } // OK: well-formed after previous line - s[0] >= 0; // OK: well-formed after previous line + ==> { assert s[0] >= 0; } // OK: well-formed after previous line + s[0] >= 0; // OK: well-formed after previous line + <==> { assert s[0] >= 0; } // OK: well-formed when the previous line is well-formed + s[0] > 0 || s[0] == 0; // OK: well-formed when the previous line is well-formed } } @@ -43,7 +45,7 @@ method CalcTest2(x: int, y: int) { } // calc expression: -function CalcTest(s: seq<int>): int { +function CalcTest3(s: seq<int>): int { calc < { 0; { assume |s| == 5; } |