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

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> {