diff options
-rw-r--r-- | Test/dafny0/Answer | 6 | ||||
-rw-r--r-- | Test/dafny0/Calculations.dfy | 16 | ||||
-rw-r--r-- | Test/dafny2/Answer | 2 | ||||
-rw-r--r-- | Test/dafny2/Calculations.dfy | 65 |
4 files changed, 84 insertions, 5 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index a5c48e9a..c738f058 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1795,12 +1795,12 @@ Calculations.dfy(8,17): Error: assertion violation Execution trace:
(0,0): anon0
(0,0): anon13_Then
-Calculations.dfy(36,11): Error: assertion violation
+Calculations.dfy(42,11): Error: assertion violation
Execution trace:
(0,0): anon0
- Calculations.dfy(31,2): anon5_Else
+ Calculations.dfy(37,2): anon5_Else
-Dafny program verifier finished with 4 verified, 4 errors
+Dafny program verifier finished with 5 verified, 4 errors
-------------------- IteratorResolution.dfy --------------------
IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field
diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy index 80775896..aa447d9f 100644 --- a/Test/dafny0/Calculations.dfy +++ b/Test/dafny0/Calculations.dfy @@ -16,6 +16,12 @@ method CalcTest0(s: seq<int>) { s[0]; } } + assume forall x :: x in s ==> x >= 0; + calc ==> { + 0 < |s|; + { assert s[0] >= 0; } // OK: well-formed after previous line + s[0] >= 0; // OK: well-formed after previous line + } } method CalcTest1(x: int, y: int) { @@ -34,4 +40,14 @@ method CalcTest2(x: int, y: int) { y + x; } assert x == 0; // error: even though assumed above, is not exported by the calculation +} + +// calc expression: +function CalcTest(s: seq<int>): int { + calc < { + 0; + { assume |s| == 5; } + |s|; + } + s[0] }
\ No newline at end of file diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index d83c766c..8e1ef967 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -57,4 +57,4 @@ Dafny program verifier finished with 36 verified, 0 errors -------------------- Calculations.dfy --------------------
-Dafny program verifier finished with 26 verified, 0 errors
+Dafny program verifier finished with 31 verified, 0 errors
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy index c637147a..79803f35 100644 --- a/Test/dafny2/Calculations.dfy +++ b/Test/dafny2/Calculations.dfy @@ -207,4 +207,67 @@ ghost method Window(xs: List, ys: List) length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(xs));
true;
}
-}
\ No newline at end of file +}
+
+// In the following we use a combination of calc and parallel
+
+function ith<a>(xs: List, i: nat): a
+ requires i < length(xs);
+{
+ match xs
+ case Cons(x, xrest) => if i == 0 then x else ith(xrest, i - 1)
+}
+
+ghost method lemma_zero_length(xs: List)
+ ensures length(xs) == 0 <==> xs.Nil?;
+{}
+
+ghost method lemma_extensionality(xs: List, ys: List)
+ requires length(xs) == length(ys); // (0)
+ requires forall i: nat | i < length(xs) :: ith(xs, i) == ith(ys, i); // (1)
+ ensures xs == ys;
+{
+ match xs {
+ case Nil =>
+ calc {
+ true;
+ // (0)
+ length(xs) == length(ys);
+ 0 == length(ys);
+ { lemma_zero_length(ys); }
+ Nil == ys;
+ xs == ys;
+ }
+ case Cons(x, xrest) =>
+ match ys {
+ case Cons(y, yrest) =>
+ calc {
+ xs;
+ Cons(x, xrest);
+ calc {
+ x;
+ ith(xs, 0);
+ // (1) with i = 0
+ ith(ys, 0);
+ y;
+ }
+ Cons(y, xrest);
+ {
+ parallel (j: nat | j < length(xrest)) {
+ calc {
+ ith(xrest, j);
+ ith(xs, j + 1);
+ // (1) with i = j + 1
+ ith(ys, j + 1);
+ ith(yrest, j);
+ }
+ }
+ lemma_extensionality(xrest, yrest);
+ }
+ Cons(y, yrest);
+ ys;
+ }
+ }
+ }
+}
+
|