From dceef1d90bfc91be2ab309107d3947ce1b3667eb Mon Sep 17 00:00:00 2001 From: rustanleino Date: Sat, 26 Mar 2011 01:58:19 +0000 Subject: Dafny: compile quantifiers Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction Dafny: split expressions when proving function postconditions Boogie and BVD: updated copyright year ranges --- Test/VSComp2010/Answer | 2 +- Test/VSComp2010/Problem4-Queens.dfy | 54 +++------------- Test/dafny0/Answer | 14 +++- Test/dafny0/NonGhostQuantifiers.dfy | 125 ++++++++++++++++++++++++++++++++++++ Test/dafny0/runtest.bat | 2 +- Test/dafny1/Answer | 2 +- Test/dafny1/Induction.dfy | 19 ++++++ 7 files changed, 167 insertions(+), 51 deletions(-) create mode 100644 Test/dafny0/NonGhostQuantifiers.dfy (limited to 'Test') 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) // 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, pos: int): bool +static function method IsConsistent(board: seq, pos: int): bool { 0 <= pos && pos < |board| && (forall q :: 0 <= q && q < pos ==> @@ -59,37 +53,6 @@ static function IsConsistent(board: seq, pos: int): bool board[pos] - board[q] != pos - q) } -method CheckConsistent(board: seq, 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) 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 { + // 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): 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): bool + { + (exists t :: t in a && (forall u :: u in a ==> u == t)) + } + function method G1(a: seq): 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): 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): 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): 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): 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): 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>): bool + { + (forall i, j :: 0 <= i && i < |S| && j in S[i] ==> 0 <= j) + } + function method Order1(S: seq>): 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) 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, 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, 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, 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) 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): 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 { -- cgit v1.2.3