Merged with default.

25 files changed, 508 insertions, 497 deletions

diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat
index 9535d677..63f5df23 100644
--- a/Test/VSComp2010/runtest.bat
+++ b/Test/VSComp2010/runtest.bat
@@ -3,8 +3,6 @@ setlocal
 

 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

 for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy

             Problem3-FindZero.dfy Problem4-Queens.dfy

diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
index 611f9251..f5b9d1b9 100644
--- a/Test/VSI-Benchmarks/runtest.bat
+++ b/Test/VSI-Benchmarks/runtest.bat
@@ -3,8 +3,6 @@ setlocal
 

 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

 for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (

   echo.

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index c451cc62..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

@@ -712,13 +714,13 @@ Modules0.dfy(7,7): Error: Duplicate name of top-level declaration: WazzupA
 Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupB

 Modules0.dfy(11,8): Error: Duplicate name of top-level declaration: WazzupB

 Modules0.dfy(12,11): Error: Duplicate name of top-level declaration: WazzupB

-Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M

+Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

+Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

+Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

+Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

+Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

 Modules0.dfy(43,13): Error: Function body type mismatch (expected T, got T)

-Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M

+Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

 Modules0.dfy(48,12): Error: new can be applied only to reference types (got T)

 Modules0.dfy(54,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)

 Modules0.dfy(70,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)

@@ -730,13 +732,20 @@ Modules0.dfy(250,15): Error: unresolved identifier: X
 Modules0.dfy(251,17): Error: member DoesNotExist does not exist in class X

 Modules0.dfy(294,16): Error: member R does not exist in class B

 Modules0.dfy(294,6): Error: expected method call, found expression

+Modules0.dfy(317,18): Error: second argument to "in" must be a set or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)

+Modules0.dfy(321,13): Error: arguments must have the same type (got Q_Imp.Node and Node)

+Modules0.dfy(322,11): Error: Undeclared module name: LongLostModule (did you forget a module import?)

+Modules0.dfy(323,11): Error: Undeclared module name: Wazzup (did you forget a module import?)

+Modules0.dfy(324,17): Error: Undeclared class name Edon in module Q_Imp

+Modules0.dfy(326,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)

+Modules0.dfy(327,30): Error: member Create does not exist in class Klassy

 Modules0.dfy(140,11): Error: ghost variables are allowed only in specification contexts

 Modules0.dfy(154,11): Error: old expressions are allowed only in specification and ghost contexts

 Modules0.dfy(155,11): Error: fresh expressions are allowed only in specification and ghost contexts

 Modules0.dfy(156,11): Error: allocated expressions are allowed only in specification and ghost contexts

 Modules0.dfy(172,10): Error: match source expression 'tree' has already been used as a match source expression in this context

 Modules0.dfy(211,12): Error: match source expression 'l' has already been used as a match source expression in this context

-30 resolution/type errors detected in Modules0.dfy

+37 resolution/type errors detected in Modules0.dfy

 

 -------------------- Modules1.dfy --------------------

 Modules1.dfy(74,16): Error: assertion violation

@@ -758,7 +767,7 @@ Modules1.dfy(58,3): Error: failure to decrease termination measure
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 19 verified, 5 errors

+Dafny program verifier finished with 22 verified, 5 errors

 

 -------------------- BadFunction.dfy --------------------

 BadFunction.dfy(6,3): Error: failure to decrease termination measure

@@ -801,14 +810,7 @@ Basics.dfy(100,16): Error: assertion violation
 Execution trace:

     (0,0): anon0

     (0,0): anon10_Then

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

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3

-    (0,0): anon11_Else

-    (0,0): anon6

-    (0,0): anon12_Then

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

+Basics.dfy(119,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must have the same value

 Execution trace:

     (0,0): anon0

     (0,0): anon10_Then

@@ -817,7 +819,7 @@ Execution trace:
     (0,0): anon6

     (0,0): anon12_Then

     (0,0): anon9

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

+Basics.dfy(133,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(145,19): Error: assertion violation

@@ -848,8 +850,11 @@ Execution trace:
     (0,0): anon13_Then

     (0,0): anon8

     (0,0): anon14_Then

+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

 

-Dafny program verifier finished with 19 verified, 11 errors

+Dafny program verifier finished with 32 verified, 11 errors

 

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

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

@@ -1567,6 +1572,11 @@ Execution trace:
 

 Dafny program verifier finished with 30 verified, 2 errors

 

+-------------------- LiberalEquality.dfy --------------------

+LiberalEquality.dfy(37,14): Error: arguments must have the same type (got Weird<T,int,V> and Weird<T,bool,V>)

+LiberalEquality.dfy(52,14): Error: arguments must have the same type (got array<int> and array<bool>)

+2 resolution/type errors detected in LiberalEquality.dfy

+

 -------------------- SmallTests.dfy --------------------

 SmallTests.dfy(30,11): Error: index out of range

 Execution trace:

@@ -1708,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

@@ -1856,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 6aa1e34d..7fca7199 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -110,7 +110,7 @@ method TestMulti(m: Multi, p: Multi)
   assert p.x == 300;

   if (*) {

     p.x, m.y := 10, 10;

-    p.x, m.x := 8, 8;  // error: duplicate assignment (since m and p may be the same)

+    p.x, m.x := 8, 8;

   }

 

   var a, b := new int[20], new int[30];

@@ -184,4 +184,59 @@ method EuclideanTest(a: int, b: int)
    assert 0 <= r < abs(b);

    assert a == b * q + r;

    assert (a/b) * b + a % b == a;

-}
\ No newline at end of file
+}

+

+method havocInMultiassignment()

+{

+   var i: nat, j: nat;

+   i, j := *, 3;

+   assert 0 <= i;

+}

+

+method m()

+{

+  var i: int, j: int;

+  i, j := 3, 6;

+  i, i := 3, 3;

+}

+

+method swap(a: array<int>, i: nat, j: nat)

+  requires a != null && 0 <= i < a.Length && 0 <= j < a.Length;

+  modifies a;

+{

+  a[i], a[j] := a[j], a[i];

+}

+

+class CC {

+  var x : int;

+  var y : int;

+}

+

+method notQuiteSwap(c: CC, d: CC)

+  requires c != null && d != null;

+  modifies c,d;

+{

+  c.x, d.x := c.x, c.x;

+}

+

+method notQuiteSwap2(c: CC, d: CC)

+  requires c != null && d != null;

+  modifies c,d;

+{

+  c.x, d.x := d.x, c.y; // BAD: c and d could be the same.

+}

+

+method OKNowIt'sSwapAgain(c: CC, d: CC)

+  requires c != null && d != null;

+  modifies c,d;

+{

+  c.x, d.x := d.x, c.x;

+}

+

+method notQuiteSwap3(c: CC, d: CC)

+  requires c != null && d != null && c != d;

+  modifies c,d;

+{

+  c.x, d.x := 4, c.y;

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

+}

diff --git a/Test/dafny0/LiberalEquality.dfy b/Test/dafny0/LiberalEquality.dfy
new file mode 100644
index 00000000..3dc52c80
--- /dev/null
+++ b/Test/dafny0/LiberalEquality.dfy
@@ -0,0 +1,55 @@
+

+class Array<T>

+{

+   var Length: nat;

+}

+

+class Test<T> {

+  var a: Array<int>;

+  var b: Array<T>;

+  predicate valid()

+      reads this, a, b;

+  {

+      a != null && b != null && a != b && a.Length == b.Length

+  }

+}

+

+method m1<T, U>(t: T, u: U)

+   requires t != u;

+{

+   

+}

+

+method m2<T>(t: array<T>, a: array<int>)

+   requires t != null && a != null && t != a && t.Length == a.Length;

+{

+

+}

+

+

+class Weird<T, U, V>

+{

+

+}

+

+

+method m3<T, V>(a: Weird<T, int, V>, b: Weird<T, bool, V>)

+   requires a == b; // Bad: second parameter can't be both bool and int.

+{

+

+}

+

+

+method m4<T, U, V>(a: Weird<T, U, V>, b: Weird<T, bool, V>)

+  requires a == b;

+{

+

+}

+

+

+// Just to make sure nothing went wrong.

+method m5(a: array<int>, b: array<bool>)

+   requires a == b; // Bad: never equal

+{

+

+}

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index b171a9c9..cc66c3c1 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -301,3 +301,31 @@ module Local imports NonLocalA, NonLocalB {
     method Q() { }

   }

 }

+

+// ------ qualified type names ----------------------------------

+

+module Q_Imp {

+  class Node { }

+  datatype List<T> = Nil | Cons(T, List);

+  class Klassy {

+    method Init()

+  }

+}

+

+module Q_M imports Q_Imp {

+  method MyMethod(root: Q_Imp.Node, S: set<Node>)

+    requires root in S;  // error: the element type of S does not agree with the type of root

+  {

+    var i := new Q_Imp.Node;

+    var j := new Node;

+    assert i != j;  // error: i and j have different types

+    var k: LongLostModule.Node;  // error: undeclared module

+    var l: Wazzup.WazzupA;  // error: undeclared module (it has not been imported)

+    var m: Q_Imp.Edon;  // error: undeclared class in module Q_Imp

+    var n: Q_Imp.List;

+    var o := new Q_Imp.List;  // error: not a class declared in module Q_Imp

+    var p := new Q_Imp.Klassy.Create();  // error: Create is not a method

+    var q := new Q_Imp.Klassy.Init();

+  }

+  class Node { }

+}

diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index 5e2d0fff..e8a88749 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -89,3 +89,23 @@ module B_Visibility imports A_Visibility {
     }

   }

 }

+

+// ------ qualified type names ----------------------------------

+

+module Q_Imp {

+  class Node { }

+  class Klassy {

+    method Init()

+  }

+}

+

+module Q_M imports Q_Imp {

+  method MyMethod(root: Q_Imp.Node, S: set<Q_Imp.Node>)

+    requires root in S;

+  {

+    var i := new Q_Imp.Node;

+    var j := new Node;

+    assert i != j;  // fine

+    var q := new Q_Imp.Klassy.Init();

+  }

+}

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/Predicates.dfy b/Test/dafny0/Predicates.dfy
index f8569b3a..146129b5 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -79,7 +79,7 @@ module Tight refines Loose {
 }

 

 module UnawareClient imports Loose {

-  method Main() {

+  method Main0() {

     var n := new MyNumber.Init();

     assert n.N == 0;  // error: this is not known

     n.Inc();

@@ -90,7 +90,7 @@ module UnawareClient imports Loose {
 }

 

 module AwareClient imports Tight {

-  method Main() {

+  method Main1() {

     var n := new MyNumber.Init();

     assert n.N == 0;

     n.Inc();

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/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index e4c134f6..ac7c8aed 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -3,7 +3,6 @@ setlocal
 

 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

 

 for %%f in (Simple.dfy) do (

   echo.

@@ -22,7 +21,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             LoopModifies.dfy Refinement.dfy RefinementErrors.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy

-            Predicates.dfy Skeletons.dfy Maps.dfy) do (

+            Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 9ed6d75a..7c7719ee 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -1,8 +1,4 @@
 

--------------------- BQueue.bpl --------------------

-

-Boogie program verifier finished with 8 verified, 0 errors

-

 -------------------- Queue.dfy --------------------

 

 Dafny program verifier finished with 22 verified, 0 errors

diff --git a/Test/dafny1/BQueue.bpl b/Test/dafny1/BQueue.bpl
deleted file mode 100644
index 77f1efb3..00000000
--- a/Test/dafny1/BQueue.bpl
+++ /dev/null
@@ -1,430 +0,0 @@
-// BQueue.bpl

-// A queue program specified in the style of dynamic frames.

-// Rustan Leino, Michal Moskal, and Wolfram Schulte, 2007.

-

-// ---------------------------------------------------------------

-

-type ref;

-const null: ref;

-

-type Field x;

-

-// this variable represents the heap; read its type as \forall \alpha. ref * Field \alpha --> \alpha

-type HeapType = <x>[ref, Field x]x;

-var H: HeapType;

-

-// every object has an 'alloc' field, which says whether or not the object has been allocated

-const unique alloc: Field bool;

-

-// for simplicity, we say that every object has one field representing its abstract value and one

-// field representing its footprint (aka frame aka data group).

-

-const unique abstractValue: Field Seq;

-const unique footprint: Field [ref]bool;

-

-// ---------------------------------------------------------------

-

-type T;  // the type of the elements of the queue

-const NullT: T;  // some value of type T

-

-// ---------------------------------------------------------------

-

-// Queue:

-const unique head: Field ref;

-const unique tail: Field ref;

-const unique mynodes: Field [ref]bool;

-// Node:

-const unique data: Field T;

-const unique next: Field ref;

-

-function ValidQueue(HeapType, ref) returns (bool);

-axiom (forall h: HeapType, q: ref ::

-  { ValidQueue(h, q) }

-  q != null && h[q,alloc] ==>

-  (ValidQueue(h, q) <==>

-     h[q,head] != null && h[h[q,head],alloc] &&

-     h[q,tail] != null && h[h[q,tail],alloc] &&

-     h[h[q,tail], next] == null &&

-     // The following line can be suppressed now that we have a ValidFootprint invariant

-     (forall o: ref :: { h[q,footprint][o] } o != null && h[q,footprint][o] ==> h[o,alloc]) &&

-     h[q,footprint][q] &&

-     h[q,mynodes][h[q,head]] && h[q,mynodes][h[q,tail]] &&

-     (forall n: ref :: { h[q,mynodes][n] }

-       h[q,mynodes][n] ==>

-           n != null && h[n,alloc] && ValidNode(h, n) &&

-           SubSet(h[n,footprint], h[q,footprint]) &&

-           !h[n,footprint][q] &&

-           (h[n,next] == null ==> n == h[q,tail])

-     ) &&

-     (forall n: ref :: { h[n,next] }

-       h[q,mynodes][n] ==>

-           (h[n,next] != null ==> h[q,mynodes][h[n,next]])

-     ) &&

-     h[q,abstractValue] == h[h[q,head],abstractValue]

-  ));

-

-// frame axiom for ValidQueue

-axiom (forall h0: HeapType, h1: HeapType, n: ref ::

-  { ValidQueue(h0,n), ValidQueue(h1,n) }

-  (forall<alpha> o: ref, f: Field alpha :: o != null && h0[o,alloc] && h0[n,footprint][o]

-      ==> h0[o,f] == h1[o,f])

-  &&

-  (forall<alpha> o: ref, f: Field alpha :: o != null && h1[o,alloc] && h1[n,footprint][o]

-      ==> h0[o,f] == h1[o,f])

-  ==>

-  ValidQueue(h0,n) == ValidQueue(h1,n));

-

-function ValidNode(HeapType, ref) returns (bool);

-axiom (forall h: HeapType, n: ref ::

-  { ValidNode(h, n) }

-  n != null && h[n,alloc] ==>

-  (ValidNode(h, n) <==>

-     // The following line can be suppressed now that we have a ValidFootprint invariant

-     (forall o: ref :: { h[n,footprint][o] } o != null && h[n,footprint][o] ==> h[o,alloc]) &&

-     h[n,footprint][n] &&

-     (h[n,next] != null ==>

-         h[h[n,next],alloc] &&

-         SubSet(h[h[n,next], footprint], h[n,footprint]) &&

-         !h[h[n,next], footprint][n]) &&

-     (h[n,next] == null ==> EqualSeq(h[n,abstractValue], EmptySeq)) &&

-     (h[n,next] != null ==> EqualSeq(h[n,abstractValue],

-                            Append(Singleton(h[h[n,next],data]), h[h[n,next],abstractValue])))

-  ));

-

-// frame axiom for ValidNode

-axiom (forall h0: HeapType, h1: HeapType, n: ref ::

-  { ValidNode(h0,n), ValidNode(h1,n) }

-  (forall<alpha> o: ref, f: Field alpha :: o != null && h0[o,alloc] && h0[n,footprint][o]

-      ==> h0[o,f] == h1[o,f])

-  &&

-  (forall<alpha> o: ref, f: Field alpha :: o != null && h1[o,alloc] && h1[n,footprint][o]

-      ==> h0[o,f] == h1[o,f])

-  ==>

-  ValidNode(h0,n) == ValidNode(h1,n));

-

-// ---------------------------------------------------------------

-

-procedure MakeQueue() returns (q: ref)

-  requires ValidFootprints(H);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySet(old(H), H, EmptySet);

-  ensures q != null && H[q,alloc];

-  ensures AllNewSet(old(H), H[q,footprint]);

-  ensures ValidQueue(H, q);

-  ensures Length(H[q,abstractValue]) == 0;

-{

-  var n: ref;

-

-  assume Fresh(H,q);

-  H[q,alloc] := true;

-

-  call n := MakeNode(NullT);

-  H[q,head] := n;

-  H[q,tail] := n;

-  H[q,mynodes] := SingletonSet(n);

-  H[q,footprint] := UnionSet(SingletonSet(q), H[n,footprint]);

-  H[q,abstractValue] := H[n,abstractValue];

-}

-

-procedure IsEmpty(q: ref) returns (isEmpty: bool)

-  requires ValidFootprints(H);

-  requires q != null && H[q,alloc] && ValidQueue(H, q);

-  ensures isEmpty <==> Length(H[q,abstractValue]) == 0;

-{

-  isEmpty := H[q,head] == H[q,tail];

-}

-

-procedure Enqueue(q: ref, t: T)

-  requires ValidFootprints(H);

-  requires q != null && H[q,alloc] && ValidQueue(H, q);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySet(old(H), H, old(H)[q,footprint]);

-  ensures DifferenceIsNew(old(H), old(H)[q,footprint], H[q,footprint]);

-  ensures ValidQueue(H, q);

-  ensures EqualSeq(H[q,abstractValue], Append(old(H)[q,abstractValue], Singleton(t)));

-{

-  var n: ref;

-

-  call n := MakeNode(t);

-

-  // foreach m in q.mynodes { m.footprint := m.footprint U n.footprint }

-  call BulkUpdateFootprint(H[q,mynodes], H[n,footprint]);

-  H[q,footprint] := UnionSet(H[q,footprint], H[n,footprint]);

-

-  // foreach m in q.mynodes { m.abstractValue := Append(m.abstractValue, Singleton(t)) }

-  call BulkUpdateAbstractValue(H[q,mynodes], t);

-  H[q,abstractValue] := H[H[q,head],abstractValue];

-

-  H[q,mynodes] := UnionSet(H[q,mynodes], SingletonSet(n));

-

-  H[H[q,tail], next] := n;

-  H[q,tail] := n;

-}

-

-procedure BulkUpdateFootprint(targetSet: [ref]bool, delta: [ref]bool);

-  requires ValidFootprints(H);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySetField(old(H), H, targetSet, footprint);

-  ensures (forall o: ref ::

-    o != null && old(H)[o,alloc] && targetSet[o]

-    ==> H[o,footprint] == UnionSet(old(H)[o,footprint], delta));

-

-procedure BulkUpdateAbstractValue(targetSet: [ref]bool, t: T);

-  requires ValidFootprints(H);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySetField(old(H), H, targetSet, abstractValue);

-  ensures (forall o: ref ::

-    o != null && old(H)[o,alloc] && targetSet[o]

-    ==> EqualSeq(H[o,abstractValue], Append(old(H)[o,abstractValue], Singleton(t))));

-

-procedure Front(q: ref) returns (t: T)

-  requires ValidFootprints(H);

-  requires q != null && H[q,alloc] && ValidQueue(H, q);

-  requires 0 < Length(H[q,abstractValue]);

-  ensures t == Index(H[q,abstractValue], 0);

-{

-  t := H[H[H[q,head], next], data];

-}

-

-procedure Dequeue(q: ref)

-  requires ValidFootprints(H);

-  requires q != null && H[q,alloc] && ValidQueue(H, q);

-  requires 0 < Length(H[q,abstractValue]);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySet(old(H), H, old(H)[q,footprint]);

-  ensures DifferenceIsNew(old(H), old(H)[q,footprint], H[q,footprint]);

-  ensures ValidQueue(H, q);

-  ensures EqualSeq(H[q,abstractValue], Drop(old(H)[q,abstractValue], 1));

-{

-  var n: ref;

-

-  n := H[H[q,head], next];

-  H[q,head] := n;

-  // we could also remove old(H)[q,head] from H[q,mynodes], and similar for the footprints

-  H[q,abstractValue] := H[n,abstractValue];

-}

-

-// --------------------------------------------------------------------------------

-

-procedure MakeNode(t: T) returns (n: ref)

-  requires ValidFootprints(H);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySet(old(H), H, EmptySet);

-  ensures n != null && H[n,alloc];

-  ensures AllNewSet(old(H), H[n,footprint]);

-  ensures ValidNode(H, n);

-  ensures H[n,data] == t && H[n,next] == null;

-{

-  assume Fresh(H,n);

-  H[n,alloc] := true;

-

-  H[n,next] := null;

-  H[n,data] := t;

-  H[n,footprint] := SingletonSet(n);

-  H[n,abstractValue] := EmptySeq;

-}

-

-// --------------------------------------------------------------------------------

-

-procedure Main(t: T, u: T, v: T)

-  requires ValidFootprints(H);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySet(old(H), H, EmptySet);

-{

-  var q0, q1: ref;

-  var w: T;

-

-  call q0 := MakeQueue();

-  call q1 := MakeQueue();

-

-  call Enqueue(q0, t);

-  call Enqueue(q0, u);

-

-  call Enqueue(q1, v);

-

-  assert Length(H[q0,abstractValue]) == 2;

-

-  call w := Front(q0);

-  assert w == t;

-  call Dequeue(q0);

-

-  call w := Front(q0);

-  assert w == u;

-

-  assert Length(H[q0,abstractValue]) == 1;

-  assert Length(H[q1,abstractValue]) == 1;

-}

-

-// --------------------------------------------------------------------------------

-

-procedure Main2(t: T, u: T, v: T, q0: ref, q1: ref)

-  requires q0 != null && H[q0,alloc] && ValidQueue(H, q0);

-  requires q1 != null && H[q1,alloc] && ValidQueue(H, q1);

-  requires DisjointSet(H[q0,footprint], H[q1,footprint]);

-  requires Length(H[q0,abstractValue]) == 0;

-

-  requires ValidFootprints(H);

-  modifies H;

-  ensures ValidFootprints(H);

-  ensures ModifiesOnlySet(old(H), H, UnionSet(old(H)[q0,footprint], old(H)[q1,footprint]));

-{

-  var w: T;

-

-  call Enqueue(q0, t);

-  call Enqueue(q0, u);

-

-  call Enqueue(q1, v);

-

-  assert Length(H[q0,abstractValue]) == 2;

-

-  call w := Front(q0);

-  assert w == t;

-  call Dequeue(q0);

-

-  call w := Front(q0);

-  assert w == u;

-

-  assert Length(H[q0,abstractValue]) == 1;

-  assert Length(H[q1,abstractValue]) == old(Length(H[q1,abstractValue])) + 1;

-}

-

-// ---------------------------------------------------------------

-

-// Helpful predicates used in specs

-

-function ModifiesOnlySet(oldHeap: HeapType, newHeap: HeapType, set: [ref]bool) returns (bool);

-axiom (forall oldHeap: HeapType, newHeap: HeapType, set: [ref]bool ::

-  { ModifiesOnlySet(oldHeap, newHeap, set) }

-  ModifiesOnlySet(oldHeap, newHeap, set) <==>

-    NoDeallocs(oldHeap, newHeap) &&

-    (forall<alpha> o: ref, f: Field alpha :: { newHeap[o,f] }

-      o != null && oldHeap[o,alloc] ==>

-      oldHeap[o,f] == newHeap[o,f] || set[o]));

-

-function ModifiesOnlySetField<alpha>(oldHeap: HeapType, newHeap: HeapType,

-                                     set: [ref]bool, field: Field alpha) returns (bool);

-axiom (forall<alpha> oldHeap: HeapType, newHeap: HeapType, set: [ref]bool, field: Field alpha ::

-  { ModifiesOnlySetField(oldHeap, newHeap, set, field) }

-  ModifiesOnlySetField(oldHeap, newHeap, set, field) <==>

-    NoDeallocs(oldHeap, newHeap) &&

-    (forall<beta> o: ref, f: Field beta :: { newHeap[o,f] }

-      o != null && oldHeap[o,alloc] ==>

-      oldHeap[o,f] == newHeap[o,f] || (set[o] && f == field)));

-

-function NoDeallocs(oldHeap: HeapType, newHeap: HeapType) returns (bool);

-axiom (forall oldHeap: HeapType, newHeap: HeapType ::

-  { NoDeallocs(oldHeap, newHeap) }

-  NoDeallocs(oldHeap, newHeap) <==>

-    (forall o: ref :: { newHeap[o,alloc] }

-      o != null && oldHeap[o,alloc] ==> newHeap[o,alloc]));

-

-function AllNewSet(oldHeap: HeapType, set: [ref]bool) returns (bool);

-axiom (forall oldHeap: HeapType, set: [ref]bool ::

-  { AllNewSet(oldHeap, set) }

-  AllNewSet(oldHeap, set) <==>

-    (forall o: ref :: { oldHeap[o,alloc] }

-      o != null && set[o] ==> !oldHeap[o,alloc]));

-

-function DifferenceIsNew(oldHeap: HeapType, oldSet: [ref]bool, newSet: [ref]bool) returns (bool);

-axiom (forall oldHeap: HeapType, oldSet: [ref]bool, newSet: [ref]bool ::

-  { DifferenceIsNew(oldHeap, oldSet, newSet) }

-  DifferenceIsNew(oldHeap, oldSet, newSet) <==>

-    (forall o: ref :: { oldHeap[o,alloc] }

-      o != null && !oldSet[o] && newSet[o] ==> !oldHeap[o,alloc]));

-

-function ValidFootprints(h: HeapType) returns (bool);

-axiom (forall h: HeapType ::

-  { ValidFootprints(h) }

-  ValidFootprints(h) <==>

-    (forall o: ref, r: ref :: { h[o,footprint][r] }

-      o != null && h[o,alloc] && r != null && h[o,footprint][r] ==> h[r,alloc]));

-

-function Fresh(h: HeapType, o: ref) returns (bool);

-axiom (forall h: HeapType, o: ref ::

-  { Fresh(h,o) }

-  Fresh(h,o) <==>

-    o != null && !h[o,alloc] && h[o,footprint] == SingletonSet(o));

-

-// ---------------------------------------------------------------

-

-const EmptySet: [ref]bool;

-axiom (forall o: ref :: { EmptySet[o] } !EmptySet[o]);

-

-function SingletonSet(ref) returns ([ref]bool);

-axiom (forall r: ref :: { SingletonSet(r) } SingletonSet(r)[r]);

-axiom (forall r: ref, o: ref :: { SingletonSet(r)[o] } SingletonSet(r)[o] <==> r == o);

-

-function UnionSet([ref]bool, [ref]bool) returns ([ref]bool);

-axiom (forall a: [ref]bool, b: [ref]bool, o: ref :: { UnionSet(a,b)[o] }

-  UnionSet(a,b)[o] <==> a[o] || b[o]);

-

-function SubSet([ref]bool, [ref]bool) returns (bool);

-axiom(forall a: [ref]bool, b: [ref]bool :: { SubSet(a,b) }

-  SubSet(a,b) <==> (forall o: ref :: {a[o]} {b[o]} a[o] ==> b[o]));

-

-function EqualSet([ref]bool, [ref]bool) returns (bool);

-axiom(forall a: [ref]bool, b: [ref]bool :: { EqualSet(a,b) }

-  EqualSet(a,b) <==> (forall o: ref :: {a[o]} {b[o]} a[o] <==> b[o]));

-

-function DisjointSet([ref]bool, [ref]bool) returns (bool);

-axiom (forall a: [ref]bool, b: [ref]bool :: { DisjointSet(a,b) }

-  DisjointSet(a,b) <==> (forall o: ref :: {a[o]} {b[o]} !a[o] || !b[o]));

-

-// ---------------------------------------------------------------

-

-// Sequence of T

-type Seq;

-

-function Length(Seq) returns (int);

-axiom (forall s: Seq :: { Length(s) } 0 <= Length(s));

-

-const EmptySeq: Seq;

-axiom Length(EmptySeq) == 0;

-axiom (forall s: Seq :: { Length(s) } Length(s) == 0 ==> s == EmptySeq);

-

-function Singleton(T) returns (Seq);

-axiom (forall t: T :: { Length(Singleton(t)) } Length(Singleton(t)) == 1);

-

-function Append(Seq, Seq) returns (Seq);

-axiom (forall s0: Seq, s1: Seq :: { Length(Append(s0,s1)) }

-  Length(Append(s0,s1)) == Length(s0) + Length(s1));

-

-function Index(Seq, int) returns (T);

-axiom (forall t: T :: { Index(Singleton(t), 0) } Index(Singleton(t), 0) == t);

-axiom (forall s0: Seq, s1: Seq, n: int :: { Index(Append(s0,s1), n) }

-  (n < Length(s0) ==> Index(Append(s0,s1), n) == Index(s0, n)) &&

-  (Length(s0) <= n ==> Index(Append(s0,s1), n) == Index(s1, n - Length(s0))));

-

-function EqualSeq(Seq, Seq) returns (bool);

-axiom (forall s0: Seq, s1: Seq :: { EqualSeq(s0,s1) }

-  EqualSeq(s0,s1) <==>

-    Length(s0) == Length(s1) &&

-    (forall j: int :: { Index(s0,j) } { Index(s1,j) }

-        0 <= j && j < Length(s0) ==> Index(s0,j) == Index(s1,j)));

-

-function Take(s: Seq, howMany: int) returns (Seq);

-axiom (forall s: Seq, n: int :: { Length(Take(s,n)) }

-  0 <= n ==>

-    (n <= Length(s) ==> Length(Take(s,n)) == n) &&

-    (Length(s) < n ==> Length(Take(s,n)) == Length(s)));

-axiom (forall s: Seq, n: int, j: int :: { Index(Take(s,n), j) }

-  0 <= j && j < n && j < Length(s) ==>

-    Index(Take(s,n), j) == Index(s, j));

-

-function Drop(s: Seq, howMany: int) returns (Seq);

-axiom (forall s: Seq, n: int :: { Length(Drop(s,n)) }

-  0 <= n ==>

-    (n <= Length(s) ==> Length(Drop(s,n)) == Length(s) - n) &&

-    (Length(s) < n ==> Length(Drop(s,n)) == 0));

-axiom (forall s: Seq, n: int, j: int :: { Index(Drop(s,n), j) }

-  0 <= n && 0 <= j && j < Length(s)-n ==>

-    Index(Drop(s,n), j) == Index(s, j+n));

-

-// ---------------------------------------------------------------

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index 1f5d78df..d098d753 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -3,14 +3,6 @@ setlocal
 

 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

-

-for %%f in (BQueue.bpl) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %BPLEXE% %* %%f

-)

 

 for %%f in (Queue.dfy PriorityQueue.dfy

             ExtensibleArray.dfy ExtensibleArrayAuto.dfy

diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index 381b9cb1..9c37549e 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -31,6 +31,22 @@ Dafny program verifier finished with 23 verified, 0 errors
 

 Dafny program verifier finished with 5 verified, 0 errors

 

+-------------------- TreeFill.dfy --------------------

+

+Dafny program verifier finished with 3 verified, 0 errors

+

+-------------------- TuringFactorial.dfy --------------------

+

+Dafny program verifier finished with 3 verified, 0 errors

+

 -------------------- StoreAndRetrieve.dfy --------------------

 

 Dafny program verifier finished with 22 verified, 0 errors

+

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

+

+Dafny program verifier finished with 11 verified, 0 errors

+

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

+

+Dafny program verifier finished with 3 verified, 0 errors

diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy
new file mode 100644
index 00000000..a7512486
--- /dev/null
+++ b/Test/dafny2/MajorityVote.dfy
@@ -0,0 +1,171 @@
+// 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

+{

+  k := a[0];

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

+  while (n < |a|)

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

+    invariant 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);

+      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 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);

+{

+  /* The postcondition of this method is proved automatically via Dafny's

+     induction tactic.  But if a manual proof had to be provided, it would

+     look like this:

+  if (s != t) {

+    Lemma_Split(a, s, t-1, u, x);

+  }

+  */

+}

+

+ghost method Lemma_Unique<T>(a: seq<T>, s: int, t: int, x: T, y: T)

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

+  ensures x != y ==> Count(a, s, t, x) + Count(a, s, t, y) <= t - s;

+{

+  /* The postcondition of this method is proved automatically via Dafny's

+     induction tactic.  But if a manual proof had to be provided, it would

+     look like this:

+  if (s != t) {

+    Lemma_Unique(a, s, t-1, x, y);

+  }

+  */

+}

diff --git a/Test/dafny2/SegmentSum.dfy b/Test/dafny2/SegmentSum.dfy
new file mode 100644
index 00000000..dc67162b
--- /dev/null
+++ b/Test/dafny2/SegmentSum.dfy
@@ -0,0 +1,29 @@
+function Sum(a: seq<int>, s: int, t: int): int

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

+{

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

+}

+

+method MaxSegSum(a: seq<int>) returns (k: int, m: int)

+  ensures 0 <= k <= m <= |a|;

+  ensures forall p,q :: 0 <= p <= q <= |a| ==> Sum(a, p, q) <= Sum(a, k, m);

+{

+  k, m := 0, 0;

+  var s := 0;  // invariant s == Sum(a, k, m)

+  var n := 0;

+  var c, t := 0, 0;  // invariant t == Sum(a, c, n)

+  while (n < |a|)

+    invariant n <= |a|;

+    invariant 0 <= c <= n && t == Sum(a, c, n);

+    invariant forall b :: 0 <= b <= n ==> Sum(a, b, n) <= Sum(a, c, n);

+    invariant 0 <= k <= m <= n && s == Sum(a, k, m);

+    invariant forall p,q :: 0 <= p <= q <= n ==> Sum(a, p, q) <= Sum(a, k, m);

+  {

+    t, n := t + a[n], n + 1;

+    if (t < 0) {

+      c, t := n, 0;

+    } else if (s < t) {

+      k, m, s := c, n, t;

+    }

+  }

+}

diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index ea26a234..15c82d65 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -1,4 +1,4 @@
-module A imports Library {

+ghost module A imports Library {

   class {:autocontracts} StoreAndRetrieve<Thing> {

     ghost var Contents: set<Thing>;

     predicate Valid

diff --git a/Test/dafny2/TreeFill.dfy b/Test/dafny2/TreeFill.dfy
new file mode 100644
index 00000000..f7e2cc89
--- /dev/null
+++ b/Test/dafny2/TreeFill.dfy
@@ -0,0 +1,27 @@
+datatype Tree<T> = Null | Node(Tree, T, Tree);

+

+function Contains<T>(t: Tree, v: T): bool

+{

+  match t

+  case Null => false

+  case Node(left, x, right) => x == v || Contains(left, v) || Contains(right, v)

+}

+

+method Fill<T>(t: Tree, a: array<T>, start: int) returns (end: int)

+  requires a != null && 0 <= start <= a.Length;

+  modifies a;

+  ensures start <= end <= a.Length;

+  ensures forall i :: 0 <= i < start ==> a[i] == old(a[i]);

+  ensures forall i :: start <= i < end ==> Contains(t, a[i]);

+{

+  match (t) {

+    case Null =>

+      end := start;

+    case Node(left, x, right) =>

+      end := Fill(left, a, start);

+      if (end < a.Length) {

+        a[end] := x;

+        end := Fill(right, a, end + 1);

+      }

+  }

+}

diff --git a/Test/dafny2/TuringFactorial.dfy b/Test/dafny2/TuringFactorial.dfy
new file mode 100644
index 00000000..585c998e
--- /dev/null
+++ b/Test/dafny2/TuringFactorial.dfy
@@ -0,0 +1,26 @@
+function Factorial(n: nat): nat

+{

+  if n == 0 then 1 else n * Factorial(n-1)

+}

+

+method ComputeFactorial(n: int) returns (u: int)

+  requires 1 <= n;

+  ensures u == Factorial(n);

+{

+  var r := 1;

+  u := 1;

+  while (r < n)  

+    invariant r <= n;

+    invariant u == Factorial(r);

+  { 

+    var v, s := u, 1;

+    while (s < r + 1)

+      invariant s <= r + 1;

+      invariant v == Factorial(r) && u == s * Factorial(r);

+    {

+      u := u + v;

+      s := s + 1;

+    }

+    r := r + 1;

+  }

+}

diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index a4796939..b68ba251 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -3,7 +3,6 @@ setlocal
 

 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

 REM soon again:    SnapshotableTrees.dfy 

 for %%f in (

@@ -14,8 +13,8 @@ for %%f in (
     COST-verif-comp-2011-2-MaxTree-datatype.dfy

     COST-verif-comp-2011-3-TwoDuplicates.dfy

     COST-verif-comp-2011-4-FloydCycleDetect.dfy

-    Intervals.dfy

-    StoreAndRetrieve.dfy

+    Intervals.dfy TreeFill.dfy TuringFactorial.dfy

+    StoreAndRetrieve.dfy MajorityVote.dfy SegmentSum.dfy

   ) do (

   echo.

   echo -------------------- %%f --------------------

diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy
index e56a8317..3e5a95ef 100644
--- a/Test/vacid0/LazyInitArray.dfy
+++ b/Test/vacid0/LazyInitArray.dfy
@@ -11,10 +11,10 @@ class LazyInitArray<T> {
     reads this, a, b, c;

   {

     a != null && b != null && c != null &&

-    a.Length == |Contents| + 1 &&  // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c'

+    a.Length == |Contents| &&

     b.Length == |Contents| &&

     c.Length == |Contents| &&

-    b != c &&

+    b != c && a != b && a != c &&

     0 <= n && n <= c.Length &&

     (forall i :: 0 <= i && i < |Contents| ==>

        Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else Zero)) &&

@@ -41,7 +41,7 @@ class LazyInitArray<T> {
     ensures |Contents| == N && Zero == zero;

     ensures (forall x :: x in Contents ==> x == zero);

   {

-    a := new T[N+1];

+    a := new T[N];

     b := new int[N];

     c := new int[N];

     n := 0;

diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat
index efe7b3d5..cd047d39 100644
--- a/Test/vacid0/runtest.bat
+++ b/Test/vacid0/runtest.bat
@@ -3,8 +3,6 @@ setlocal
 

 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

 for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (

   echo.

diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat
index 770f41dc..7f7c9b9f 100644
--- a/Test/vstte2012/runtest.bat
+++ b/Test/vstte2012/runtest.bat
@@ -3,7 +3,6 @@ setlocal
 

 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

 for %%f in (

     Two-Way-Sort.dfy