merge

17 files changed, 492 insertions, 17 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 1ac8fc1c..e0874a66 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -198,8 +198,18 @@ Execution trace:
     (0,0): anon0

     SmallTests.dfy(267,19): anon3_Else

     (0,0): anon2

+SmallTests.dfy(307,3): Error BP5003: A postcondition might not hold on this return path.

+SmallTests.dfy(301,11): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon18_Else

+    (0,0): anon11

+    (0,0): anon23_Then

+    (0,0): anon24_Then

+    (0,0): anon15

+    (0,0): anon25_Else

 

-Dafny program verifier finished with 34 verified, 13 errors

+Dafny program verifier finished with 41 verified, 14 errors

 

 -------------------- Definedness.dfy --------------------

 Definedness.dfy(8,7): Error: possible division by zero

@@ -391,6 +401,13 @@ Execution trace:
 

 Dafny program verifier finished with 3 verified, 3 errors

 

+-------------------- ResolutionErrors.dfy --------------------

+ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops

+ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)

+ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)

+ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)

+4 resolution/type errors detected in ResolutionErrors.dfy

+

 -------------------- Array.dfy --------------------

 Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause

 Execution trace:

@@ -457,14 +474,17 @@ 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'

-NonGhostQuantifiers.dfy(120,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-8 resolution/type errors detected in NonGhostQuantifiers.dfy

+NonGhostQuantifiers.dfy(42,4): 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(46,4): 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 'd'

+NonGhostQuantifiers.dfy(50,4): 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(74,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(78,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(88,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(103,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(111,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(120,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'

+NonGhostQuantifiers.dfy(137,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+11 resolution/type errors detected in NonGhostQuantifiers.dfy

 

 -------------------- AdvancedLHS.dfy --------------------

 AdvancedLHS.dfy(32,23): Error: target object may be null

@@ -483,9 +503,12 @@ Modules0.dfy(62,6): Error: inter-module calls must follow the module import rela
 Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)

 Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)

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

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

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

-10 resolution/type errors detected in Modules0.dfy

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

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

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

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

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

+13 resolution/type errors detected in Modules0.dfy

 

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

 Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0

@@ -504,6 +527,59 @@ Execution trace:
 

 Dafny program verifier finished with 2 verified, 1 error

 

+-------------------- Comprehensions.dfy --------------------

+Comprehensions.dfy(9,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon9_Then

+    (0,0): anon10_Then

+    (0,0): anon4

+    (0,0): anon11_Then

+    (0,0): anon12_Then

+    (0,0): anon8

+

+Dafny program verifier finished with 6 verified, 1 error

+

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

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+    (0,0): anon7_Else

+    (0,0): anon8_Else

+    (0,0): anon9_Then

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+    (0,0): anon7_Else

+    (0,0): anon8_Then

+ControlStructures.dfy(14,3): Error: missing case in case statement: Purple

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+    (0,0): anon7_Else

+    (0,0): anon8_Then

+ControlStructures.dfy(43,5): Error: missing case in case statement: Red

+Execution trace:

+    (0,0): anon0

+    (0,0): anon8_Then

+    (0,0): anon9_Else

+    (0,0): anon10_Then

+ControlStructures.dfy(51,3): Error: missing case in case statement: Red

+Execution trace:

+    (0,0): anon8_Else

+    (0,0): anon9_Else

+    (0,0): anon10_Else

+    (0,0): anon11_Else

+    (0,0): anon12_Then

+ControlStructures.dfy(72,3): Error: alternative cases fail to cover all possibilties

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

+

+Dafny program verifier finished with 15 verified, 6 errors

+

 -------------------- Termination.dfy --------------------

 Termination.dfy(102,3): Error: cannot prove termination; try supplying a decreases clause for the loop

 Execution trace:

diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy
new file mode 100644
index 00000000..8629a418
--- /dev/null
+++ b/Test/dafny0/Comprehensions.dfy
@@ -0,0 +1,40 @@
+method M()

+{

+  var numbers := set i | 0 <= i && i < 100;

+  var squares := set i | 0 <= i && i < 100 :: Id(i)*i;  // verifying properties about set comprehensions with a term expression is hard

+

+  assert 12 in numbers;

+  assert Id(5) == 5;

+  assert 25 in squares;

+  assert 200 in numbers;  // error

+}

+

+function method Id(x: int): int { x }  // for triggering

+

+// The following mainly test that set comprehensions can be compiled, but one would

+// have to run the resulting program to check that the compiler is doing the right thing.

+method Main()

+{

+  var q := set i,j | 0 <= i && i < 10 && 0 <= j && j < 3 :: i+j;

+  call PrintSet(q);

+  q := set b: bool | true :: if b then 3 else 7;

+  call PrintSet(q);

+  var m := set k | k in q :: 2*k;

+  call PrintSet(m);

+  call PrintSet(set k | k in q && k % 2 == 0);

+  var sq := [30, 40, 20];

+  call PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);

+  var bb := forall k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i == 17;

+}

+

+method PrintSet<T>(s: set<T>) {

+  var q := s;

+  while (q != {})

+    decreases q;

+  {

+    var x := choose q;

+    print x, " ";

+    q := q - {x};

+  }

+  print "\n";

+}

diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy
new file mode 100644
index 00000000..35d939d3
--- /dev/null
+++ b/Test/dafny0/ControlStructures.dfy
@@ -0,0 +1,137 @@
+datatype D = Green | Blue | Red | Purple;

+

+method M0(d: D)

+{

+  match (d) {  // error: two missing cases: Blue and Purple

+    case Green =>

+    case Red =>

+  }

+}

+

+method M1(d: D)

+  requires d != #D.Blue;

+{

+  match (d) {  // error: missing case: Purple

+    case Green =>

+    case Red =>

+  }

+}

+

+method M2(d: D)

+  requires d != #D.Blue && d != #D.Purple;

+{

+  match (d) {

+    case Green =>

+    case Red =>

+  }

+}

+

+method M3(d: D)

+  requires d == #D.Green;

+{

+  if (d != #D.Green) {

+    match (d) {

+      // nothing here

+    }

+  }

+}

+

+method M4(d: D)

+  requires d == #D.Green || d == #D.Red;

+{

+  if (d != #D.Green) {

+    match (d) {  // error: missing case Red

+      // nothing here

+    }

+  }

+}

+

+function F0(d: D): int

+{

+  match (d)  // error: missing cases Red

+  case Purple => 80

+  case Green => 0

+  case Blue => 2

+}

+

+function F1(d: D, x: int): int

+  requires x < 100;

+  requires d == #D.Red ==> x == 200;  // (an impossibility, given the first precondition, so d != Red)

+{

+  match (d)

+  case Purple => 80

+  case Green => 0

+  case Blue => 2

+}

+

+// --------------- alternative statements ---------------------

+

+method A0(x: int) returns (r: int)

+  ensures 0 <= r;

+{

+  if {  // error: missing case (x == 0)

+    case x < 0 => r := 12;

+    case 0 < x => r := 13;

+  }

+}

+

+method A1(x: int) returns (r: int)

+  ensures 0 <= r;

+{

+  if {

+    case x <= 0 => r := 12;

+    case 0 <= x => r := 13;

+  }

+}

+

+method DutchFlag(A: array<int>, N: int, l: int, r: int) returns (result: int)

+  requires A != null && N == A.Length;

+  requires 0 <= l && l+2 <= r && r <= N;

+  modifies A;

+  ensures l <= result && result < r;

+  ensures forall k, j :: l <= k && k < result && result <= j && j < r ==> A[k] <= A[j];

+  ensures forall k :: l <= k && k < result ==> A[k] <= old(A[l]);

+  ensures forall k :: result <= k && k < r ==> old(A[l]) <= A[k];

+{

+  var pv := A[l];

+  var i := l;

+  var j := r-1;

+  // swap A[l] and A[j]

+  var tmp := A[l]; A[l] := A[j]; A[j] := tmp;

+

+  while (i < j)

+    invariant l <= i && i <= j && j < r;

+    invariant forall k :: l <= k && k < i ==> A[k] <= pv;

+    invariant forall k :: j <= k && k < r ==> pv <= A[k];

+  {

+    if {

+      case A[i] <= pv =>

+        i := i + 1;

+      case pv <= A[j-1] =>

+        j := j - 1;

+      case A[j-1] < pv && pv < A[i] =>

+        // swap A[j-1] and A[i]

+        tmp := A[i]; A[i] := A[j-1]; A[j-1] := tmp;

+        assert A[i] < pv && pv < A[j-1];

+        i := i + 1;

+        j := j - 1;

+    }

+  }

+  result := i;

+}

+

+// --------------- alternative loop statements  ---------------

+

+method B(x: int) returns (r: int)

+  ensures r == 0;

+{

+  r := x;

+  while

+    decreases if 0 <= r then r else -r;

+  {

+    case r < 0 =>

+      r := r + 1;

+    case 0 < r =>

+      r := r - 1;

+  }

+}

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index adce71a8..59052ac2 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -121,6 +121,21 @@ class Ghosty {
   ghost method Theorem(a: int) { }

 }

 

+var SomeField: int;

+

+method SpecialFunctions()

+  modifies this;

+{

+  SomeField := SomeField + 4;

+  var a := old(SomeField);  // error: old can only be used in ghost contexts

+  var b := fresh(this);  // error: fresh can only be used in ghost contexts

+  var c := allocated(this);  // error: allocated can only be used in ghost contexts

+  if (fresh(this)) {  // this guard makes the if statement a ghost statement

+    ghost var x := old(SomeField);  // this is a ghost context, so it's okay

+    ghost var y := allocated(this);  // this is a ghost context, so it's okay

+  }

+}

+

 // ---------------------- illegal match expressions ---------------

 

 datatype Tree { Nil; Cons(int, Tree, Tree); }

diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 93bd4b65..6b7ce9b9 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -60,7 +60,7 @@ datatype List<T> {
   Cons(nat, T, List<T>);

 }

 

-method MatchIt(list: List<bool>) returns (k: nat)

+method MatchIt(list: List<object>) returns (k: nat)

 {

   match (list) {

     case Nil =>

diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy
index ea256a58..58e64827 100644
--- a/Test/dafny0/NonGhostQuantifiers.dfy
+++ b/Test/dafny0/NonGhostQuantifiers.dfy
@@ -33,6 +33,23 @@ class MyClass<T> {
     (forall n :: 2 <= n ==> 1000 <= n || (exists d :: n < d && d < 2*n))

   }

 

+  function method GoodRange(): bool

+  {

+    (forall n | 2 <= n :: 1000 <= n || (exists d | n < d :: d < 2*n)) && (exists K: nat | K < 100 :: true)

+  }

+  function method BadRangeForall(): bool

+  {

+    forall n | n <= 2 :: 1000 <= n || n % 2 == 0  // error: cannot bound range for n

+  }

+  function method BadRangeExists(): bool

+  {

+    exists d | d < 1000 :: d < 2000  // error: cannot bound range for d

+  }

+  function method WhatAboutThis(): bool

+  {

+    forall n :: 2 <= n && (forall M | M == 1000 :: n < M) ==> n % 2 == 0  // error: heuristics don't get this one for n

+  }

+

   // Here are more tests

 

   function method F(a: array<T>): bool

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
new file mode 100644
index 00000000..5ec0cc4c
--- /dev/null
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -0,0 +1,25 @@
+

+//Should not verify, as ghost loops should not be allowed to diverge.

+method GhostDivergentLoop()

+{

+   var a := new int [2];

+   a[0] := 1;

+   a[1] := -1;

+   ghost var i := 0;

+   while (i < 2)

+      decreases *; // error: not allowed on a ghost loop

+	  invariant i <= 2;

+	  invariant (forall j :: 0 <= j && j < i ==> a[j] > 0);

+   {

+     i := 0;

+   }

+   assert a[1] != a[1]; // ...for then this would incorrectly verify

+}

+

+method M<T>(a: array3<T>, b: array<T>, m: int, n: int)

+{

+  // the following invalid expressions were once incorrectly resolved:

+  var x := a[m, n];        // error

+  var y := a[m];           // error

+  var z := b[m, n, m, n];  // error

+}

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index a839d5a9..a5f02dc6 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -272,3 +272,49 @@ class InitCalls {
     r := new InitCalls.InitFromReference(r);  // error, since r.z is unknown

   }

 }

+

+// --------------- some tests with quantifiers and ranges ----------------------

+

+method QuantifierRange0<T>(a: seq<T>, x: T, y: T, N: int)

+  requires 0 <= N && N <= |a|;

+  requires forall k | 0 <= k && k < N :: a[k] != x;

+  requires exists k | 0 <= k && k < N :: a[k] == y;

+  ensures forall k :: 0 <= k && k < N ==> a[k] != x;  // same as the precondition, but using ==> instead of |

+  ensures exists k :: 0 <= k && k < N && a[k] == y;  // same as the precondition, but using && instead of |

+{

+  assert x != y;

+}

+

+method QuantifierRange1<T>(a: seq<T>, x: T, y: T, N: int)

+  requires 0 <= N && N <= |a|;

+  requires forall k :: 0 <= k && k < N ==> a[k] != x;

+  requires exists k :: 0 <= k && k < N && a[k] == y;

+  ensures forall k | 0 <= k && k < N :: a[k] != x;  // same as the precondition, but using | instead of ==>

+  ensures exists k | 0 <= k && k < N :: a[k] == y;  // same as the precondition, but using | instead of &&

+{

+  assert x != y;

+}

+

+method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int)

+  requires 0 <= N && N <= |a|;

+  requires exists k | 0 <= k && k < N :: a[k] == y;

+  ensures forall k | 0 <= k && k < N :: a[k] == y;  // error

+{

+  assert N != 0;

+  if (N == 1) {

+    assert forall k | a[if 0 <= k && k < N then k else 0] != y :: k < 0 || N <= k;  // in this case, the precondition holds trivially

+  }

+  if (forall k | 0 <= k && k < N :: a[k] == x) {

+    assert x == y;

+  }

+}

+

+// ----------------------- tests that involve sequences of boxed booleans --------

+

+ghost method M(zeros: seq<bool>, Z: bool)

+  requires 1 <= |zeros| && Z == false;

+  requires forall k :: 0 <= k && k < |zeros| ==> zeros[k] == Z;

+{

+  var x := [Z];

+  assert zeros[0..1] == [Z];

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 491b7b75..16bc0e2b 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -11,10 +11,11 @@ for %%f in (Simple.dfy) do (
   %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f

 )

 

-for %%f in (TypeTests.dfy NatTypes.dfy  SmallTests.dfy Definedness.dfy

-            FunctionSpecifications.dfy

+for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy

+            FunctionSpecifications.dfy ResolutionErrors.dfy

             Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

+            Comprehensions.dfy ControlStructures.dfy

             Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

             Refinement.dfy RefinementErrors.dfy) do (

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index d96e12a5..0111f9af 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -59,9 +59,13 @@ Dafny program verifier finished with 2 verified, 0 errors
 

 Dafny program verifier finished with 17 verified, 0 errors

 

+-------------------- FindZero.dfy --------------------

+

+Dafny program verifier finished with 4 verified, 0 errors

+

 -------------------- TerminationDemos.dfy --------------------

 

-Dafny program verifier finished with 11 verified, 0 errors

+Dafny program verifier finished with 14 verified, 0 errors

 

 -------------------- Substitution.dfy --------------------

 

diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy
new file mode 100644
index 00000000..cff8b934
--- /dev/null
+++ b/Test/dafny1/FindZero.dfy
@@ -0,0 +1,30 @@
+method FindZero(a: array<int>) returns (r: int)

+  requires a != null && forall i :: 0 <= i && i < a.Length ==> 0 <= a[i];

+  requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

+  ensures 0 <= r ==> r < a.Length && a[r] == 0;

+  ensures r < 0 ==> forall i :: 0 <= i && i < a.Length ==> a[i] != 0;

+{

+  var n := 0;

+  while (n < a.Length)

+    invariant forall i :: 0 <= i && i < n && i < a.Length ==> a[i] != 0;

+  {

+    if (a[n] == 0) { r := n; return; }

+    call Lemma(a, n, a[n]);

+    n := n + a[n];

+  }

+  r := -1;

+}

+

+ghost method Lemma(a: array<int>, k: int, m: int)

+  requires a != null && forall i :: 0 <= i && i < a.Length ==> 0 <= a[i];

+  requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

+  requires 0 <= k;

+  requires k < a.Length ==> m <= a[k];

+  ensures forall i :: k <= i && i < k+m && i < a.Length ==> a[i] != 0;

+  decreases m;

+{

+  if (0 < m && k < a.Length) {

+    assert a[k] != 0;

+    call Lemma(a, k+1, m-1);

+  }

+}

diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy
index 01a7c7bd..49f5a075 100644
--- a/Test/dafny1/TerminationDemos.dfy
+++ b/Test/dafny1/TerminationDemos.dfy
@@ -42,6 +42,28 @@ class Ackermann {
     else

       G(m - 1, G(m, n - 1))

   }

+

+  function H(m: nat, n: nat): nat

+  {

+    if m == 0 then

+      n + 1

+    else if n == 0 then

+      H(m - 1, 1)

+    else

+      H(m - 1, H(m, n - 1))

+  }

+

+  method ComputeAck(m: nat, n: nat) returns (r: nat)

+  {

+    if (m == 0) {

+      r := n + 1;

+    } else if (n == 0) {

+      call r := ComputeAck(m - 1, 1);

+    } else {

+      call s := ComputeAck(m, n - 1);

+      call r := ComputeAck(m - 1, s);

+    }

+  }

 }

 

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

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index 36b93883..57ac97e3 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -19,7 +19,7 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy
             ListCopy.dfy ListReverse.dfy ListContents.dfy

             MatrixFun.dfy pow2.dfy

             SchorrWaite.dfy

-            Cubes.dfy SumOfCubes.dfy

+            Cubes.dfy SumOfCubes.dfy FindZero.dfy

             TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy

             Induction.dfy Rippling.dfy

             Celebrity.dfy

diff --git a/Test/test0/Answer b/Test/test0/Answer
index 0441b69b..d434a8ca 100644
--- a/Test/test0/Answer
+++ b/Test/test0/Answer
@@ -247,3 +247,16 @@ BadQuantifier.bpl(3,15): error: invalid QuantifierBody
 EmptyCallArgs.bpl(31,2): Error: type variable must occur in types of given arguments: a

 EmptyCallArgs.bpl(32,2): Error: type variable must occur in types of given arguments: a

 2 name resolution errors detected in EmptyCallArgs.bpl

+----- SeparateVerification0.bpl

+SeparateVerification0.bpl(13,6): Error: undeclared identifier: y

+1 name resolution errors detected in SeparateVerification0.bpl

+----- SeparateVerification1.bpl SeparateVerification0.bpl

+SeparateVerification1.bpl(4,6): Error: undeclared identifier: x

+SeparateVerification0.bpl(10,6): Error: undeclared identifier: x

+2 name resolution errors detected in SeparateVerification0.bpl

+----- SeparateVerification0.bpl SeparateVerification0.bpl

+

+Boogie program verifier finished with 0 verified, 0 errors

+----- SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl

+

+Boogie program verifier finished with 0 verified, 0 errors

diff --git a/Test/test0/SeparateVerification0.bpl b/Test/test0/SeparateVerification0.bpl
new file mode 100644
index 00000000..5a8ef283
--- /dev/null
+++ b/Test/test0/SeparateVerification0.bpl
@@ -0,0 +1,21 @@
+// need to include this file twice for it to include all necessary declarations

+

+#if FILE_0

+const x: int;

+#else

+const y: int;

+#endif

+

+#if FILE_1

+axiom x == 12;

+procedure Q();

+#else

+axiom y == 7;

+#endif

+

+// duplicates of :extern's are fine (Boogie keeps the non-:extern or chooses arbitrarily among the :extern's)

+type {:extern} T;

+const {:extern} C: int;

+function {:extern} F(): int;

+var {:extern} n: int;

+procedure {:extern} P(inconsistentParameterButThatIsOkayBecauseTheExternIsIgnored: int);

diff --git a/Test/test0/SeparateVerification1.bpl b/Test/test0/SeparateVerification1.bpl
new file mode 100644
index 00000000..0e3e7926
--- /dev/null
+++ b/Test/test0/SeparateVerification1.bpl
@@ -0,0 +1,19 @@
+// to be used with SeparateVerification0.bpl

+

+// x and y are declared in SeparateVerification0.bpl

+axiom x + y <= 100;

+

+// these are declared as :extern as SeparateVerification0.bpl

+type T;

+const C: int;

+function F(): int;

+var n: int;

+procedure P();

+procedure {:extern} Q(x: int);

+

+procedure Main() {

+  call P();  // note, calling the parameter-less non-extern P (an extern and a non-extern

+             // declaration of the same name are usually mostly identical declarations,

+             // but Boogie allows them to be different, because it ignores the extern ones)

+  call Q();  // ditto

+}

diff --git a/Test/test0/runtest.bat b/Test/test0/runtest.bat
index c7c6ee3d..5ecc22dc 100644
--- a/Test/test0/runtest.bat
+++ b/Test/test0/runtest.bat
@@ -31,3 +31,12 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe
 %BGEXE% %* /noVerify Orderings.bpl

 %BGEXE% %* /noVerify BadQuantifier.bpl

 %BGEXE% %* /noVerify EmptyCallArgs.bpl

+

+echo ----- SeparateVerification0.bpl

+%BGEXE% %* /noVerify SeparateVerification0.bpl

+echo ----- SeparateVerification1.bpl SeparateVerification0.bpl

+%BGEXE% %* /noVerify SeparateVerification1.bpl SeparateVerification0.bpl

+echo ----- SeparateVerification0.bpl SeparateVerification0.bpl

+%BGEXE% %* /noVerify SeparateVerification0.bpl SeparateVerification0.bpl

+echo ----- SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl

+%BGEXE% %* /noVerify SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl