Merge

7 files changed, 161 insertions, 40 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index bc653bd3..5f80df86 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -91,8 +91,10 @@ TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the
 TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type

 TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type

 TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type

+TypeTests.dfy(116,4): Error: cannot assign to non-ghost variable in a ghost context

+TypeTests.dfy(117,7): Error: cannot assign to non-ghost variable in a ghost context

 TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

-34 resolution/type errors detected in TypeTests.dfy

+36 resolution/type errors detected in TypeTests.dfy

 

 -------------------- NatTypes.dfy --------------------

 NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative

@@ -280,7 +282,7 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-SmallTests.dfy(584,18): Error: target object may be null

+SmallTests.dfy(584,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

 SmallTests.dfy(597,10): Error: assertion violation

@@ -851,11 +853,8 @@ Execution trace:
 Basics.dfy(226,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value

 Execution trace:

     (0,0): anon0

-Basics.dfy(251,6): Error: left-hand sides 0 and 1 refer to the same location

-Execution trace:

-    (0,0): anon0

 

-Dafny program verifier finished with 35 verified, 12 errors

+Dafny program verifier finished with 32 verified, 11 errors

 

 -------------------- ControlStructures.dfy --------------------

 ControlStructures.dfy(5,3): Error: missing case in case statement: Blue

@@ -1719,7 +1718,7 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-SmallTests.dfy(584,18): Error: target object may be null

+SmallTests.dfy(584,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

 SmallTests.dfy(597,10): Error: assertion violation

@@ -1867,7 +1866,7 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-out.tmp.dfy(530,18): Error: target object may be null

+out.tmp.dfy(530,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

 out.tmp.dfy(543,10): Error: assertion violation

diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index 87a984a3..7fca7199 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -240,14 +240,3 @@ method notQuiteSwap3(c: CC, d: CC)
   c.x, d.x := 4, c.y;

   c.x, c.y := 3, c.y;

 }

-

-method M() returns (a: int, b: int) {

-  return 4, 6;

-}

-method otherChecks()

-{

-  var x: int, y: int;

-  x, y :| x + y == 5; // fine

-  x, x :| x + y == 5; // BAD, must give different variables.

-  //x, x := M(); // <-- this is caught early, so it suppresses other errors.

-}
\ No newline at end of file
diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
index ab711d02..f260edb5 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy
+++ b/Test/dafny0/ParallelResolveErrors.dfy
@@ -103,6 +103,6 @@ method M1() {
 method M2() {

   var a := new int[100];

   parallel (x | 0 <= x < 100) {

-    a[x] :| a[x] > 0;  // error: not allowed to update heap location in a parallel statement with a(n implicit) assume

+    a[x] :| assume a[x] > 0;  // error: not allowed to update heap location in a parallel statement with an assume

   }

 }

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 4d219cd3..e8b618d7 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -542,21 +542,21 @@ method AssignSuchThat0(a: int, b: int) returns (x: int, y: int)
   ensures x == a && y == b;

 {

   if (*) {

-    x, y :| a <= x < a + 1 && b + a <= y + a && y <= b;

+    x, y :| assume a <= x < a + 1 && b + a <= y + a && y <= b;

   } else {

-    var xx, yy :| a <= xx < a + 1 && b + a <= yy + a && yy <= b;

+    var xx, yy :| assume a <= xx < a + 1 && b + a <= yy + a && yy <= b;

     x, y := xx, yy;

   }

 }

 

 method AssignSuchThat1(a: int, b: int) returns (x: int, y: int)

 {

-  var k :| 0 <= k < a - b;  // this acts like an 'assume 0 < a - b;'

+  var k :| assume 0 <= k < a - b;  // this acts like an 'assume 0 < a - b;'

   assert b < a;

-  k :| k == old(2*k);  // note, the 'old' has no effect on local variables like k

+  k :| assume k == old(2*k);  // note, the 'old' has no effect on local variables like k

   assert k == 0;

   var S := {2, 4, 7};

-  var T :| T <= S;

+  var T :| assume T <= S;

   assert 3 !in T;

   assert T == {};  // error: T may be larger

 }

@@ -568,38 +568,38 @@ method AssignSuchThat2(i: int, j: int, ghost S: set<Node>)
   var a := new int[25];

   var t;

   if (0 <= i < j < 25) {

-    a[i], t, a[j], n.next, n :| true;

+    a[i], t, a[j], n.next, n :| assume true;

   }

   if (n != null && n.next != null) {

     assume n in S && n.next in S;

-    n.next.next, n.next :| n != null && n.next != null && n.next.next == n.next;  // error: n.next may equal n (thus aliasing n.next.next and n.next)

+    n.next.next, n.next :| assume n != null && n.next != null && n.next.next == n.next;  // error: n.next may equal n (thus aliasing n.next.next and n.next)

   } else if (0 <= i < 25 && 0 <= j < 25) {

-    t, a[i], a[j] :| t < a[i] < a[j];  // error: i may equal j (thus aliasing a[i] and a[j])

+    t, a[i], a[j] :| assume t < a[i] < a[j];  // error: i may equal j (thus aliasing a[i] and a[j])

   }

 }

 

 method AssignSuchThat3()

 {

   var n := new Node;

-  n, n.next :| n.next == n;  // error: RHS is not well defined (RHS is evaluated after the havocking of the LHS)

+  n, n.next :| assume n.next == n;  // error: RHS is not well defined (RHS is evaluated after the havocking of the LHS)

 }

 

 method AssignSuchThat4()

 {

   var n := new Node;

-  n, n.next :| n != null && n.next == n;  // that's the ticket

+  n, n.next :| assume n != null && n.next == n;  // that's the ticket

 }

 

 method AssignSuchThat5()

 {

   var n := new Node;

-  n :| fresh(n);  // fine

+  n :| assume fresh(n);  // fine

   assert false;  // error

 }

 

 method AssignSuchThat6()

 {

   var n: Node;

-  n :| n != null && fresh(n);  // there is no non-null fresh object, so this amounts to 'assume false;'

+  n :| assume n != null && fresh(n);  // there is no non-null fresh object, so this amounts to 'assume false;'

   assert false;  // no problemo

 }

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 29274381..8434f06c 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -92,3 +92,28 @@ method K(s: set<nat>) {  // error: not allowed to instantiate 'set' with 'nat'
   var b := new nat[100,200];  // error: not allowed the type array2<nat>

 }

 

+// --------------------- more ghost tests, for assign-such-that statements

+

+method M()

+{

+  ghost var b: bool;

+  ghost var k: int, l: int;

+  var m: int;

+

+  // These three statements are allowed by the resolver, but the compiler will complain

+  // if it ever gets them.

+  k :| k < 10;

+  k, m :| 0 <= k < m;

+  m :| m < 10;

+

+  // Because of the ghost guard, these 'if' statements are ghost contexts, so only

+  // assignments to ghosts are allowed.

+  if (b) {

+    k :| k < 10;  // should be allowed

+    k, l :| 0 <= k < l;  // ditto

+  }

+  if (b) {

+    m :| m < 10;  // error: not allowed in ghost context

+    k, m :| 0 <= k < m;  // error: not allowed in ghost context

+  }

+}

diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index b0bbfe05..93524dfa 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -41,7 +41,7 @@ Dafny program verifier finished with 22 verified, 0 errors
 

 -------------------- MajorityVote.dfy --------------------

 

-Dafny program verifier finished with 7 verified, 0 errors

+Dafny program verifier finished with 11 verified, 0 errors

 

 -------------------- SegmentSum.dfy --------------------

 

diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy
index 0adba718..a7512486 100644
--- a/Test/dafny2/MajorityVote.dfy
+++ b/Test/dafny2/MajorityVote.dfy
@@ -1,3 +1,62 @@
+// Rustan Leino, June 2012.

+// This file verifies an algorithm, due to Boyer and Moore, that finds the majority choice

+// among a sequence of votes, see http://www.cs.utexas.edu/~moore/best-ideas/mjrty/.

+// Actually, this algorithm is a slight variation on theirs, but the general idea for why

+// it is correct is the same.  In the Boyer and Moore algorithm, the loop counter is advanced

+// by exactly 1 each iteration, which means that there may or may not be a "current leader".

+// In my program below, I had instead written the loop invariant to say there is always a

+// "current leader", which requires the loop index sometimes to skip a value.

+//

+// This file has two versions of the algorithm.  In the first version, the given sequence

+// of votes is assumed to have a (strict) majority choice, meaning that strictly more than

+// 50% of the votes are for one candidate.  It is convenient to have a name for the majority

+// choice, in order to talk about it in specifications.  The easiest way to do this in

+// Dafny is probably to introduce a ghost parameter with the given properties.  That's what

+// the algorithm does, see parameter K.  The postcondition is thus to output the value of

+// K, which is done in the non-ghost out-parameter k.

+// The proof of the algorithm requires two lemmas.  These lemmas are proved automatically

+// by Dafny's induction tactic.

+//

+// In the second version of the program, the main method does not assume there is a majority

+// choice.  Rather, it eseentially uses the first algorithm and then checks if what it

+// returns really is a majority choice.  To do this, the specification of the first algorithm

+// needs to be changed slightly to accommodate the possibility that there is no majority

+// choice.  That change in specification is also reflected in the loop invariant.  Moreover,

+// the algorithm itself now needs to extra 'if' statements to see if the entire sequence

+// has been searched through.  (This extra 'if' is essentially already handled by Boyer and

+// Moore's algorithm, because it increments the loop index by 1 each iteration and therefore

+// already has a special case for the case of running out of sequence elements without a

+// current leader.)

+// The calling harness, DetermineElection, somewhat existentially comes up with the majority

+// choice, if there is such a choice, and then passes in that choice as the ghost parameter K

+// to the main algorithm.  Neat, huh?

+

+// Advanced remark:

+// There is a subtle situation in the verification of DetermineElection.  Suppose the type

+// parameter Candidate denotes some type whose instances depend on which object are

+// allocated.  For example, if Candidate is some class type, then more candidates can come

+// into being by object allocations (using "new").  What does the quantification of

+// candidates "c" in the postcondition of DetermineElection now mean--all candidates that

+// existed in the pre-state or (the possibly larger set of) all candidates that exist in the

+// post-state?  (It means the latter.)  And if there does not exist a candidate in majority

+// in the pre-state, could there be a (newly created) candidate in majority in the post-state?

+// This will require some proof.  The simplest argument seems to be that even if more candidates

+// are created during the course of DetermineElection, such candidates cannot possibly

+// be in majority in the sequence "a", since "a" can only contain candidates that were already

+// created in the pre-state.  This property is easily specified by adding a postcondition

+// to the Count function.  Alternatively, one could have added the antecedent "c in a" or

+// "old(allocated(c))" to the "forall c" quantification in the postcondition of DetermineElection.

+

+function method Count<T>(a: seq<T>, s: int, t: int, x: T): int

+  requires 0 <= s <= t <= |a|;

+  ensures Count(a, s, t, x) == 0 || x in a;

+{

+  if s == t then 0 else

+  Count(a, s, t-1, x) + if a[t-1] == x then 1 else 0

+}

+

+// Here is the first version of the algorithm, the one that assumes there is a majority choice.

+

 method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k: Candidate)

   requires 2 * Count(a, 0, |a|, K) > |a|;  // K has a (strict) majority of the votes

   ensures k == K;  // find K

@@ -29,6 +88,62 @@ method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k:
   Lemma_Unique(a, s, |a|, K, k);  // both k and K have a majority, so K == k

 }

 

+// ------------------------------------------------------------------------------

+

+// Here is the second version of the program, the one that also computes whether or not

+// there is a majority choice.

+

+method DetermineElection<Candidate>(a: seq<Candidate>) returns (hasWinner: bool, cand: Candidate)

+  ensures hasWinner ==> 2 * Count(a, 0, |a|, cand) > |a|;

+  ensures !hasWinner ==> forall c :: 2 * Count(a, 0, |a|, c) <= |a|;

+{

+  ghost var b := exists c :: 2 * Count(a, 0, |a|, c) > |a|;

+  ghost var w :| b ==> 2 * Count(a, 0, |a|, w) > |a|;

+  cand := SearchForWinner(a, b, w);

+  return 2 * Count(a, 0, |a|, cand) > |a|, cand;

+}

+

+// The difference between SearchForWinner for FindWinner above are the occurrences of the

+// antecedent "hasWinner ==>" and the two checks for no-more-votes that may result in a "return"

+// statement.

+

+method SearchForWinner<Candidate>(a: seq<Candidate>, ghost hasWinner: bool, ghost K: Candidate) returns (k: Candidate)

+  requires hasWinner ==> 2 * Count(a, 0, |a|, K) > |a|;  // K has a (strict) majority of the votes

+  ensures hasWinner ==> k == K;  // find K

+{

+  if (|a| == 0) { return; }

+  k := a[0];

+  var n, c, s := 1, 1, 0;

+  while (n < |a|)

+    invariant 0 <= s <= n <= |a|;

+    invariant hasWinner ==> 2 * Count(a, s, |a|, K) > |a| - s;  // K has majority among a[s..]

+    invariant 2 * Count(a, s, n, k) > n - s;  // k has majority among a[s..n]

+    invariant c == Count(a, s, n, k);

+  {

+    if (a[n] == k) {

+      n, c := n + 1, c + 1;

+    } else if (2 * c > n + 1 - s) {

+      n := n + 1;

+    } else {

+      n := n + 1;

+      // We have 2*Count(a, s, n, k) == n-s, and thus the following lemma

+      // lets us conclude 2*Count(a, s, n, K) <= n-s.

+      Lemma_Unique(a, s, n, K, k);

+      // We also have 2*Count(a, s, |a|, K) > |a|-s, and the following lemma

+      // tells us Count(a, s, |a|, K) == Count(a, s, n, K) + Count(a, n, |a|, K),

+      // and thus we can conclude 2*Count(a, n, |a|, K) > |a|-n.

+      Lemma_Split(a, s, n, |a|, K);

+      if (|a| == n) { return; }

+      k, n, c, s := a[n], n + 1, 1, n;

+    }

+  }

+  Lemma_Unique(a, s, |a|, K, k);  // both k and K have a majority, so K == k

+}

+

+// ------------------------------------------------------------------------------

+

+// Here are two lemmas about Count that are used in the methods above.

+

 ghost method Lemma_Split<T>(a: seq<T>, s: int, t: int, u: int, x: T)

   requires 0 <= s <= t <= u <= |a|;

   ensures Count(a, s, t, x) + Count(a, t, u, x) == Count(a, s, u, x);

@@ -54,10 +169,3 @@ ghost method Lemma_Unique<T>(a: seq<T>, s: int, t: int, x: T, y: T)
   }

   */

 }

-

-function Count<T>(a: seq<T>, s: int, t: int, x: T): int

-  requires 0 <= s <= t <= |a|;

-{

-  if s == t then 0 else

-  Count(a, s, t-1, x) + if a[t-1] == x then 1 else 0

-}