diff options
| author |  Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2013-02-15 17:07:57 -0800 |
|---|---|---|
| committer | Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2013-02-15 17:07:57 -0800 |
| commit | 5c5d0318c70d53eb8b287b07edfce96b6888a540 (patch) | |
| tree | 8f8673d8201258232ee5074e3411dc8a1f642570 /Test/dafny2 | |
| parent | 79d90df7412bf52276280bf82b478dc11cd8b0ed (diff) | |
Added tests: parallel calc, better well-formedness checks, calc expression.
Diffstat (limited to 'Test/dafny2')
| -rw-r--r-- | Test/dafny2/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny2/Calculations.dfy | 65 |
2 files changed, 65 insertions, 2 deletions
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;
+ }
+ }
+ }
+}
+
|