summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/VSComp2010/Answer2
-rw-r--r--Test/VSComp2010/Problem4-Queens.dfy54
-rw-r--r--Test/dafny0/Answer14
-rw-r--r--Test/dafny0/NonGhostQuantifiers.dfy125
-rw-r--r--Test/dafny0/runtest.bat2
-rw-r--r--Test/dafny1/Answer2
-rw-r--r--Test/dafny1/Induction.dfy19
7 files changed, 167 insertions, 51 deletions
diff --git a/Test/VSComp2010/Answer b/Test/VSComp2010/Answer
index 50f20679..dc523fdf 100644
--- a/Test/VSComp2010/Answer
+++ b/Test/VSComp2010/Answer
@@ -16,7 +16,7 @@ Compiled program written to out.cs
-------------------- Problem4-Queens.dfy --------------------
-Dafny program verifier finished with 11 verified, 0 errors
+Dafny program verifier finished with 9 verified, 0 errors
Compiled program written to out.cs
-------------------- Problem5-DoubleEndedQueue.dfy --------------------
diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy
index e73c644f..ef084674 100644
--- a/Test/VSComp2010/Problem4-Queens.dfy
+++ b/Test/VSComp2010/Problem4-Queens.dfy
@@ -1,5 +1,5 @@
// VSComp 2010, problem 4, N queens
-// Rustan Leino, 31 August 2010.
+// Rustan Leino, 31 August 2010, updated 24 March 2011.
//
// In the version of this program that I wrote during the week of VSTTE 2010, I had
// an unproved assumption. In this version, I simply changed the existential quantifier
@@ -11,17 +11,7 @@
// The correctness of this program relies on some properties of Queens boards. These
// are stated and proved as lemmas, which here are given in assert statements.
//
-// There are two annoyances in this program:
-//
-// One has to do with Dafny's split between ''ghost'' variables/code and ''physical''
-// variables/code. The ''ghost'' things are used by the verifier, but are ignored by
-// the compiler. This is generally good, since any additional specifications are ghost
-// state that are needed to convince the verifier that a program is correct (let alone
-// express what it means for the program to be correct) are not required at run time.
-// However, Dafny currently considers *all* quantifiers to be ghost-only, which
-// necessitates some duplication of the 'IsConsistent' condition.
-//
-// The other annoyance is that Dafny's proof-term representation of the function
+// There is an annoyance in this program. Dafny's proof-term representation of the function
// 'IsConsistent' implicitly takes the heap as an argument, despite the fact that
// 'IsConsistent' does not depend on any part of the heap. Dafny ought to be able
// to figure that out from the fact that 'IsConsistent' has no 'reads' clause.
@@ -29,6 +19,10 @@
// below are specified with an (easy-to-prove) postcondition that 'IsConsistent(B,p)'
// does not change for any 'B' and 'p', even if the method may change the heap in
// some way.
+//
+// The March 2011 update of this program was to make use of Dafny's new heuristics for
+// compiling quantifiers. This makes it possible to call IsConsistent, whose body uses
+// a universal quantifier, from non-ghost code, which simplifies this program.
// The Search method returns whether or not there exists an N-queens solution for the
@@ -50,7 +44,7 @@ method Search(N: int) returns (success: bool, board: seq<int>)
// Given a board, this function says whether or not the queen placed in column 'pos'
// is consistent with the queens placed in columns to its left.
-static function IsConsistent(board: seq<int>, pos: int): bool
+static function method IsConsistent(board: seq<int>, pos: int): bool
{
0 <= pos && pos < |board| &&
(forall q :: 0 <= q && q < pos ==>
@@ -59,37 +53,6 @@ static function IsConsistent(board: seq<int>, pos: int): bool
board[pos] - board[q] != pos - q)
}
-method CheckConsistent(board: seq<int>, pos: int) returns (b: bool)
- ensures b <==> IsConsistent(board, pos);
- ensures (forall B, p :: IsConsistent(B, p) <==> old(IsConsistent(B, p)));
-{
- // The Dafny compiler won't compile a function with a 'forall' inside. (This seems reasonable
- // in general, since quantifiers could range over all the integers. Here, however, where the
- // range of the quantifier is bounded, it just seems stupid.) Therefore, we
- // have to provide a method that computes the same thing as the function defines.
- if (0 <= pos && pos < |board|) {
- var p := 0;
- while (p < pos)
- invariant p <= pos;
- invariant (forall q :: 0 <= q && q < p ==>
- board[q] != board[pos] &&
- board[q] - board[pos] != pos - q &&
- board[pos] - board[q] != pos - q);
- {
- if (!(board[p] != board[pos] &&
- board[p] - board[pos] != pos - p &&
- board[pos] - board[p] != pos - p)) {
- b := false;
- return;
- }
- p := p + 1;
- }
- b := true;
- return;
- }
- b := false;
-}
-
// Here comes the method where the real work is being done. With an ultimate board size of 'N'
// in mind and given the consistent placement 'boardSoFar' of '|boardSoFar|' columns, this method
// will search for a solution for the remaining columns. If 'success' returns as 'true',
@@ -135,8 +98,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard:
{
// Let's try to extend the board-so-far with a queen in column 'n':
var candidateBoard := boardSoFar + [n];
- call consistent := CheckConsistent(candidateBoard, pos);
- if (consistent) {
+ if (IsConsistent(candidateBoard, pos)) {
// The new queen is consistent. Thus, 'candidateBoard' is consistent in column 'pos'.
// The consistency of the queens in columns left of 'pos' follows from the
// consistency of those queens in 'boardSoFar' and the fact that 'candidateBoard' is
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index c33cf851..b1e12099 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -295,7 +295,7 @@ Execution trace:
Definedness.dfy(208,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-Definedness.dfy(231,30): Error: possible violation of function postcondition
+Definedness.dfy(231,46): Error: possible violation of function postcondition
Execution trace:
(0,0): anon0
(0,0): anon5_Else
@@ -321,7 +321,7 @@ Execution trace:
(0,0): anon13_Else
(0,0): anon7
(0,0): anon9
-FunctionSpecifications.dfy(40,18): Error: possible violation of function postcondition
+FunctionSpecifications.dfy(40,24): Error: possible violation of function postcondition
Execution trace:
(0,0): anon12_Else
(0,0): anon15_Else
@@ -399,6 +399,16 @@ Execution trace:
Dafny program verifier finished with 8 verified, 2 errors
+-------------------- NonGhostQuantifiers.dfy --------------------
+NonGhostQuantifiers.dfy(13,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(57,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
+NonGhostQuantifiers.dfy(61,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(71,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(86,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(94,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
+NonGhostQuantifiers.dfy(103,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
+7 resolution/type errors detected in NonGhostQuantifiers.dfy
+
-------------------- Modules0.dfy --------------------
Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
Modules0.dfy(13,7): Error: module T named among imports does not exist
diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy
new file mode 100644
index 00000000..dd730e90
--- /dev/null
+++ b/Test/dafny0/NonGhostQuantifiers.dfy
@@ -0,0 +1,125 @@
+// This file contains various tests of resolving quantifiers in ghost and non-ghost positions
+
+class MyClass<T> {
+ // This function is in a ghost context, so all is cool.
+ function GhostF(): bool
+ {
+ (forall n :: 2 <= n ==> (exists d :: n < d && d < 2*n))
+ }
+ // But try to make it a non-ghost function, and Dafny will object because it cannot compile the
+ // body into code that will terminate.
+ function method NonGhostF(): bool
+ {
+ (forall n :: 2 <= n ==> (exists d :: n < d && d < 2*n)) // error: can't figure out how to compile
+ }
+ // Add an upper bound to n and things are cool again.
+ function method NonGhostF_Bounded(): bool
+ {
+ (forall n :: 2 <= n && n < 1000 ==> (exists d :: n < d && d < 2*n))
+ }
+ // Although the heuristics applied are syntactic, they do see through the structure of the boolean
+ // operators ==>, &&, ||, and !. Hence, the following three variations of the previous function can
+ // also be compiled.
+ function method NonGhostF_Or(): bool
+ {
+ (forall n :: !(2 <= n && n < 1000) || (exists d :: n < d && d < 2*n))
+ }
+ function method NonGhostF_ImpliesImplies(): bool
+ {
+ (forall n :: 2 <= n ==> n < 1000 ==> (exists d :: n < d && d < 2*n))
+ }
+ function method NonGhostF_Shunting(): bool
+ {
+ (forall n :: 2 <= n ==> 1000 <= n || (exists d :: n < d && d < 2*n))
+ }
+
+ // Here are more tests
+
+ function method F(a: array<T>): bool
+ requires a != null;
+ reads a;
+ {
+ (exists i :: 0 <= i && i < a.Length / 2 && (forall j :: i <= j && j < a.Length ==> a[i] == a[j]))
+ }
+
+ function method G0(a: seq<T>): bool
+ {
+ (exists t :: t in a && (forall u :: u in a ==> u == t))
+ }
+ function method G1(a: seq<T>): bool
+ {
+ (exists ti :: 0 <= ti && ti < |a| && (forall ui :: 0 <= ui && ui < |a| ==> a[ui] == a[ti]))
+ }
+
+ // Regrettably, the heuristics don't know about transitivity:
+ function method IsSorted0(s: seq<int>): bool
+ {
+ (forall i, j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) // error: can't figure out how to compile
+ }
+ function method IsSorted1(s: seq<int>): bool
+ {
+ (forall j, i :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) // error: can't figure out how to compile
+ }
+ // Add the redundant conjunct "i < |s|" and things are fine.
+ function method IsSorted2(s: seq<int>): bool
+ {
+ (forall i, j :: 0 <= i && i < |s| && i < j && j < |s| ==> s[i] <= s[j])
+ }
+ // But if you switch the order of i and j, you need a different redundant conjunct.
+ function method IsSorted3(s: seq<int>): bool
+ {
+ (forall j, i :: 0 <= i && i < |s| && i < j && j < |s| ==> s[i] <= s[j]) // error: can't figure out how to compile
+ }
+ function method IsSorted4(s: seq<int>): bool
+ {
+ (forall j, i :: 0 <= i && 0 < j && i < j && j < |s| ==> s[i] <= s[j])
+ }
+
+ // The heuristics look at bound variables in the order given, as is illustrated by the following
+ // two functions.
+ function method Order0(S: seq<set<int>>): bool
+ {
+ (forall i, j :: 0 <= i && i < |S| && j in S[i] ==> 0 <= j)
+ }
+ function method Order1(S: seq<set<int>>): bool
+ {
+ (forall j, i :: 0 <= i && i < |S| && j in S[i] ==> 0 <= j) // error: can't figure out how to compile
+ }
+
+ // Quantifiers can be used in other contexts, too.
+ // For example, in assert statements and assignment statements.
+ method M(s: seq<int>) returns (r: bool, q: bool) {
+ assert (forall x :: x in s ==> 0 <= x);
+ r := (forall x :: x in s ==> x < 100);
+ q := (exists y :: y*y in s); // error: can't figure out how to compile
+ }
+ // And if expressions.
+ function method Select_Good(S: set<int>, a: T, b: T): T
+ {
+ if (forall x :: x in S ==> 0 <= x && x < 100) then a else b
+ }
+ function method Select_Bad(S: set<int>, a: T, b: T): T
+ {
+ if (forall x :: x*x in S ==> 0 <= x && x < 100) then a else b // error: can't figure out how to compile
+ }
+ // (the same thing, but in a ghost function is fine, though)
+ function Select_Bad_Ghost(S: set<int>, a: T, b: T): T
+ {
+ if (forall x :: x*x in S ==> 0 <= x && x < 100) then a else b
+ }
+ // And if statements
+/****
+ method N(s: seq<int>) returns (ghost g: int, h: int)
+ {
+ if ( (forall x :: x in s ==> 0 <= x) ) {
+ h := 0; g := 0;
+ }
+ if ( (forall x :: x*x in s ==> x < 100) ) { // this is fine, since the whole statement is a ghost statement
+ g := 2;
+ }
+ if ( (forall x :: x*x in s ==> x < 50) ) { // error: cannot compile this guard of a non-ghost if statement
+ h := 6;
+ }
+ }
+****/
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 3e9507ef..2c55a6b9 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -12,7 +12,7 @@ for %%f in (Simple.dfy) do (
)
for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy FunctionSpecifications.dfy
- Array.dfy MultiDimArray.dfy
+ Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy
Modules0.dfy Modules1.dfy BadFunction.dfy
Termination.dfy Use.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 4bf200cd..d9b32305 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -73,7 +73,7 @@ Dafny program verifier finished with 6 verified, 0 errors
-------------------- Induction.dfy --------------------
-Dafny program verifier finished with 22 verified, 0 errors
+Dafny program verifier finished with 23 verified, 0 errors
-------------------- Rippling.dfy --------------------
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 4bd1f35b..f31d79f8 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -107,6 +107,25 @@ class IntegerInduction {
call Theorem4();
}
}
+
+ // The body of this function method gives a single quantifier, which leads to an efficient
+ // way to check sortedness at run time. However, an alternative, and ostensibly more general,
+ // way to express sortedness is given in the function's postcondition. The alternative
+ // formulation may be easier to understand for a human and may also be more readily applicable
+ // for the program verifier. Dafny will show that postcondition holds, which ensures the
+ // equivalence of the two formulations.
+ // The proof of the postcondition requires induction. It would have been nicer to state it
+ // as one formula of the form "IsSorted(s) <==> ...", but then Dafny would never consider the
+ // possibility of applying induction. Instead, the "==>" and "<==" cases are given separately.
+ // Proving the "<==" case is simple; it's the "==>" case that requires induction.
+ // The example uses an attribute that requests induction on just "j". However, the proof also
+ // goes through by applying induction just on "i" or applying induction on both bound variables.
+ function method IsSorted(s: seq<int>): bool
+ ensures IsSorted(s) ==> (forall i,j {:induction j} :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]);
+ ensures (forall i,j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) ==> IsSorted(s);
+ {
+ (forall i :: 0 <= i && i+1 < |s| ==> s[i] <= s[i+1])
+ }
}
datatype Tree<T> {
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 22:53:47 +0000