diff options
Diffstat (limited to 'Test/dafny0/Calculations.dfy')
-rw-r--r-- | Test/dafny0/Calculations.dfy | 10 |
1 files changed, 6 insertions, 4 deletions
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; } |