summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/VSComp2010/Problem2-Invert.dfy1
-rw-r--r--Test/dafny0/Answer54
-rw-r--r--Test/dafny0/Calculations.dfy37
-rw-r--r--Test/dafny0/CoPredicates.dfy11
-rw-r--r--Test/dafny0/ParseErrors.dfy58
-rw-r--r--Test/dafny0/ResolutionErrors.dfy29
-rw-r--r--Test/dafny0/runtest.bat2
-rw-r--r--Test/dafny2/Answer4
-rw-r--r--Test/dafny2/Calculations.dfy209
-rw-r--r--Test/dafny2/runtest.bat2
10 files changed, 390 insertions, 17 deletions
diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy
index 2a262d70..0f7c50c1 100644
--- a/Test/VSComp2010/Problem2-Invert.dfy
+++ b/Test/VSComp2010/Problem2-Invert.dfy
@@ -43,6 +43,7 @@ method M(N: int, A: array<int>, B: array<int>)
assert (forall i :: 0 <= i && i < N ==> A[i] == old(A[i])); // the elements of A were not changed by the loop
// it now follows from the surjectivity of A that A is the inverse of B:
assert (forall j :: 0 <= j && j < N && inImage(j) ==> 0 <= B[j] && B[j] < N && A[B[j]] == j);
+ assert (forall j,k :: 0 <= j && j < k && k < N ==> B[j] != B[k]);
}
static function inImage(i: int): bool { true } // this function is used to trigger the surjective quantification
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 671c7c91..140f642f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -332,10 +332,10 @@ Execution trace:
Definedness.dfy(86,5): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause
+Definedness.dfy(86,10): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(86,10): Error: target object may be null
+Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
Definedness.dfy(87,10): Error: possible violation of function precondition
@@ -542,7 +542,16 @@ ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specificat
ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
-48 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(363,4): Error: arguments to + must be int or a collection type (instead got bool)
+ResolutionErrors.dfy(368,4): Error: all lines in a calculation must have the same type (got int after bool)
+ResolutionErrors.dfy(371,4): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(371,4): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(372,8): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(372,8): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(377,8): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(377,8): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(382,4): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+57 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
@@ -553,7 +562,13 @@ ParseErrors.dfy(15,18): error: this operator cannot be part of a chain
ParseErrors.dfy(16,19): error: this operator cannot be part of a chain
ParseErrors.dfy(17,18): error: this operator cannot be part of a chain
ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
-8 parse errors detected in ParseErrors.dfy
+ParseErrors.dfy(46,8): error: the main operator of a calculation must be transitive
+ParseErrors.dfy(62,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(63,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(68,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(69,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(75,2): error: this operator cannot continue this calculation
+14 parse errors detected in ParseErrors.dfy
-------------------- Array.dfy --------------------
Array.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause
@@ -857,19 +872,19 @@ Execution trace:
Dafny program verifier finished with 32 verified, 11 errors
-------------------- ControlStructures.dfy --------------------
-ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
+ControlStructures.dfy(5,3): Error: missing case in case statement: Purple
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
- (0,0): anon8_Else
- (0,0): anon9_Then
-ControlStructures.dfy(5,3): Error: missing case in case statement: Purple
+ (0,0): anon8_Then
+ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
- (0,0): anon8_Then
+ (0,0): anon8_Else
+ (0,0): anon9_Then
ControlStructures.dfy(14,3): Error: missing case in case statement: Purple
Execution trace:
(0,0): anon0
@@ -1305,7 +1320,7 @@ CoPredicates.dfy(30,22): Related location: Related location
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 14 verified, 1 error
+Dafny program verifier finished with 12 verified, 1 error
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
@@ -1615,6 +1630,25 @@ TailCalls.dfy(42,12): Error: 'decreases *' is allowed only on tail-recursive met
TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive methods
5 resolution/type errors detected in TailCalls.dfy
+-------------------- Calculations.dfy --------------------
+Calculations.dfy(3,4): Error: index out of range
+Execution trace:
+ (0,0): anon0
+ (0,0): anon11_Then
+Calculations.dfy(8,13): Error: index out of range
+Execution trace:
+ (0,0): anon0
+ (0,0): anon13_Then
+Calculations.dfy(8,17): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon13_Then
+Calculations.dfy(36,11): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ Calculations.dfy(31,2): anon5_Else
+
+Dafny program verifier finished with 4 verified, 4 errors
-------------------- IteratorResolution.dfy --------------------
IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field
IteratorResolution.dfy(64,18): Error: arguments must have the same type (got _T0 and int)
diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy
new file mode 100644
index 00000000..9e44f62e
--- /dev/null
+++ b/Test/dafny0/Calculations.dfy
@@ -0,0 +1,37 @@
+method CalcTest0(s: seq<int>) {
+ calc {
+ s[0]; // error: ill-formed line
+ }
+
+ calc {
+ 2;
+ { assert s[0] == 1; } // error: ill-formed hint
+ 1 + 1;
+ }
+
+ if (|s| > 0) {
+ calc {
+ s[0]; // OK: well-formed in this context
+ { assert s[0] == s[0]; }
+ <= s[0];
+ }
+ }
+}
+
+method CalcTest1(x: int, y: int) {
+ calc {
+ x + y;
+ { assume x == 0; }
+ y;
+ }
+ assert x == 0; // OK: follows from x + y == y;
+}
+
+method CalcTest2(x: int, y: int) {
+ calc {
+ x + y;
+ { assume x == 0; }
+ y + x;
+ }
+ assert x == 0; // error: even though assumed above, is not exported by the calculation
+} \ No newline at end of file
diff --git a/Test/dafny0/CoPredicates.dfy b/Test/dafny0/CoPredicates.dfy
index 67dff91b..c5651c90 100644
--- a/Test/dafny0/CoPredicates.dfy
+++ b/Test/dafny0/CoPredicates.dfy
@@ -51,8 +51,9 @@ function U2(n: int): Stream<int>
UpwardBy2(n)
}
-ghost method Lemma2(n: int)
- ensures Even(UpwardBy2(2*n)); // this is true, but Dafny can't prove it
-{
- assert Even(U2(2*n)); // ... thanks to this lemma
-}
+// Postponed:
+//ghost method Lemma2(n: int)
+// ensures Even(UpwardBy2(2*n)); // this is true, and Dafny can prove it
+//{
+// assert Even(U2(2*n)); // ... thanks to this lemma
+//}
diff --git a/Test/dafny0/ParseErrors.dfy b/Test/dafny0/ParseErrors.dfy
index 41df50eb..9a3cc18b 100644
--- a/Test/dafny0/ParseErrors.dfy
+++ b/Test/dafny0/ParseErrors.dfy
@@ -18,3 +18,61 @@ method TestChaining1<T>(s: set<T>, t: set<T>, u: set<T>, x: T, SuperSet: set<set
ensures x in s == t; // error: 'in' is not chaining
{
}
+
+// ---------------------- calc statements -----------------------------------
+
+method TestCalc()
+{
+ calc {} // OK, empty calculations are allowed
+ calc {
+ 2 + 3; // OK, single-line calculations are allowed
+ }
+ calc {
+ 2 + 3;
+ calc { // OK: a calc statement is allowed as a sub-hint
+ 2;
+ 1 + 1;
+ }
+ calc {
+ 3;
+ 1 + 2;
+ }
+ { assert true; } // OK: multiple subhints are allowed between two lines
+ 1 + 1 + 1 + 2;
+ { assert 1 + 1 + 1 == 3; }
+ { assert true; }
+ 3 + 2;
+ }
+ calc != { // error: != is not allowed as the main operator of a calculation
+ 2 + 3;
+ 4;
+ }
+ calc { // OK, these operators are compatible
+ 2 + 3;
+ > 4;
+ >= 2 + 2;
+ }
+ calc < { // OK, these operators are compatible
+ 2 + 3;
+ == 5;
+ <= 3 + 3;
+ }
+ calc < { // error: cannot mix < and >= or >
+ 2 + 3;
+ >= 5;
+ > 2 + 2;
+ 6;
+ }
+ calc >= { // error: cannot mix >= and <= or !=
+ 2 + 3;
+ <= 5;
+ != 2 + 2;
+ 3;
+ }
+ calc { // error: cannot have more than one != per calc
+ 2 + 3;
+ != 4;
+ != 1 + 2;
+ 3;
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 274cc95a..c615c5ec 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -354,3 +354,32 @@ method MG1(l: GList, n: nat)
var t := GCons(100, GNil);
t := GCons(120, l); // error: types don't match up (List<T$0> versus List<int>)
}
+
+// ------------------- calc statements ------------------------------
+
+method TestCalc(m: int, n: int, a: bool, b: bool)
+{
+ calc {
+ a + b; // error: invalid line
+ n + m;
+ }
+ calc {
+ a && b;
+ n + m; // error: all lines must have the same type
+ }
+ calc ==> {
+ n + m; // error: ==> operator requires boolean lines
+ n + m + 1;
+ n + m + 2;
+ }
+ calc {
+ n + m;
+ n + m + 1;
+ ==> n + m + 2; // error: ==> operator requires boolean lines
+ }
+ calc {
+ n + m;
+ { print n + m; } // error: non-ghost statements are not allowed in hints
+ m + n;
+ }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 9789e7d7..9118e388 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -24,7 +24,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy
RefinementModificationChecking.dfy TailCalls.dfy
- IteratorResolution.dfy Iterators.dfy) do (
+ Calculations.dfy IteratorResolution.dfy Iterators.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index 447f4365..2feaf6f7 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -54,3 +54,7 @@ Dafny program verifier finished with 3 verified, 0 errors
-------------------- MonotonicHeapstate.dfy --------------------
Dafny program verifier finished with 36 verified, 0 errors
+
+-------------------- Calculations.dfy --------------------
+
+Dafny program verifier finished with 26 verified, 0 errors
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy
new file mode 100644
index 00000000..8c13457b
--- /dev/null
+++ b/Test/dafny2/Calculations.dfy
@@ -0,0 +1,209 @@
+/* Lists */
+// Here are some standard definitions of List and functions on Lists
+
+datatype List<T> = Nil | Cons(T, List);
+
+function length(l: List): nat
+{
+ match l
+ case Nil => 0
+ case Cons(x, xs) => 1 + length(xs)
+}
+
+function concat(l: List, ys: List): List
+{
+ match l
+ case Nil => ys
+ case Cons(x, xs) => Cons(x, concat(xs, ys))
+}
+
+function reverse(l: List): List
+{
+ match l
+ case Nil => Nil
+ case Cons(x, xs) => concat(reverse(xs), Cons(x, Nil))
+}
+
+function revacc(l: List, acc: List): List
+{
+ match l
+ case Nil => acc
+ case Cons(x, xs) => revacc(xs, Cons(x, acc))
+}
+
+function qreverse(l: List): List
+{
+ revacc(l, Nil)
+}
+
+// Here are two lemmas about the List functions.
+
+ghost method Lemma_ConcatNil()
+ ensures forall xs :: concat(xs, Nil) == xs;
+{
+}
+
+ghost method Lemma_RevCatCommute()
+ ensures forall xs, ys, zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs);
+{
+}
+
+// Here is a theorem that says "qreverse" and "reverse" calculate the same result. The proof
+// is given in a calculational style. The proof is not minimal--some lines can be omitted
+// and Dafny will still fill in the details.
+
+ghost method Theorem_QReverseIsCorrect_Calc(l: List)
+ ensures qreverse(l) == reverse(l);
+{
+ calc {
+ qreverse(l);
+ // def. qreverse
+ revacc(l, Nil);
+ { Lemma_Revacc_calc(l, Nil); }
+ concat(reverse(l), Nil);
+ { Lemma_ConcatNil(); }
+ reverse(l);
+ }
+}
+
+ghost method Lemma_Revacc_calc(xs: List, ys: List)
+ ensures revacc(xs, ys) == concat(reverse(xs), ys);
+{
+ match (xs) {
+ case Nil =>
+ case Cons(x, xrest) =>
+ calc {
+ concat(reverse(xs), ys);
+ // def. reverse
+ concat(concat(reverse(xrest), Cons(x, Nil)), ys);
+ // induction hypothesis: Lemma_Revacc_calc(xrest, Cons(x, Nil))
+ concat(revacc(xrest, Cons(x, Nil)), ys);
+ { Lemma_RevCatCommute(); } // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)
+ revacc(xrest, concat(Cons(x, Nil), ys));
+ // def. concat (x2)
+ revacc(xrest, Cons(x, ys));
+ // def. revacc
+ revacc(xs, ys);
+ }
+ }
+}
+
+// Here is a version of the same proof, as it was constructed before Dafny's "calc" construct.
+
+ghost method Theorem_QReverseIsCorrect(l: List)
+ ensures qreverse(l) == reverse(l);
+{
+ assert qreverse(l)
+ == // def. qreverse
+ revacc(l, Nil);
+ Lemma_Revacc(l, Nil);
+ assert revacc(l, Nil)
+ == concat(reverse(l), Nil);
+ Lemma_ConcatNil();
+}
+
+ghost method Lemma_Revacc(xs: List, ys: List)
+ ensures revacc(xs, ys) == concat(reverse(xs), ys);
+{
+ match (xs) {
+ case Nil =>
+ case Cons(x, xrest) =>
+ assert revacc(xs, ys)
+ == // def. revacc
+ revacc(xrest, Cons(x, ys));
+
+ assert concat(reverse(xs), ys)
+ == // def. reverse
+ concat(concat(reverse(xrest), Cons(x, Nil)), ys)
+ == // induction hypothesis: Lemma3a(xrest, Cons(x, Nil))
+ concat(revacc(xrest, Cons(x, Nil)), ys);
+ Lemma_RevCatCommute(); // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)
+ assert concat(revacc(xrest, Cons(x, Nil)), ys)
+ == revacc(xrest, concat(Cons(x, Nil), ys));
+
+ assert forall g, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs);
+
+ assert revacc(xrest, concat(Cons(x, Nil), ys))
+ == // the assert lemma just above
+ revacc(xrest, Cons(x, ys));
+ }
+}
+
+/* Fibonacci */
+// To further demonstrate what the "calc" construct can do, here are some proofs about the Fibonacci function.
+
+function Fib(n: nat): nat
+{
+ if n < 2 then n else Fib(n - 2) + Fib(n - 1)
+}
+
+ghost method Lemma_Fib()
+ ensures Fib(5) < 6;
+{
+ calc {
+ Fib(5);
+ Fib(4) + Fib(3);
+ calc {
+ Fib(2);
+ Fib(0) + Fib(1);
+ 0 + 1;
+ 1;
+ }
+ < 6;
+ }
+}
+
+/* List length */
+// Here are some proofs that show the use of nested calculations.
+
+ghost method Lemma_Concat_Length(xs: List, ys: List)
+ ensures length(concat(xs, ys)) == length(xs) + length(ys);
+{}
+
+ghost method Lemma_Reverse_Length(xs: List)
+ ensures length(xs) == length(reverse(xs));
+{
+ match (xs) {
+ case Nil =>
+ case Cons(x, xrest) =>
+ calc {
+ length(reverse(xs));
+ // def. reverse
+ length(concat(reverse(xrest), Cons(x, Nil)));
+ { Lemma_Concat_Length(reverse(xrest), Cons(x, Nil)); }
+ length(reverse(xrest)) + length(Cons(x, Nil));
+ // induction hypothesis
+ length(xrest) + length(Cons(x, Nil));
+ calc {
+ length(Cons(x, Nil));
+ // def. length
+ 1 + length(Nil);
+ // def. length
+ 1 + 0;
+ 1;
+ }
+ length(xrest) + 1;
+ // def. length
+ length(xs);
+ }
+ }
+}
+
+ghost method Window(xs: List, ys: List)
+ ensures length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(ys));
+{
+ calc {
+ length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(ys));
+ { if (length(xs) == length(ys)) {
+ calc {
+ length(reverse(xs));
+ { Lemma_Reverse_Length(xs); }
+ length(xs);
+ length(ys);
+ { Lemma_Reverse_Length(ys); }
+ length(reverse(ys));
+ } } }
+ length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(xs));
+ true;
+ }
+} \ No newline at end of file
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index 909f67f5..72959830 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -16,7 +16,7 @@ for %%f in (
StoreAndRetrieve.dfy
Intervals.dfy TreeFill.dfy TuringFactorial.dfy
MajorityVote.dfy SegmentSum.dfy
- MonotonicHeapstate.dfy
+ MonotonicHeapstate.dfy Calculations.dfy
) do (
echo.
echo -------------------- %%f --------------------
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 02:03:11 +0000