Dafny:

* added missing error checking for ghost-vs-physical contexts (e.g., use of the "old" keyword)
* check that arrays are not null when accessed
* added dafny1/FindZero.dfy test case

6 files changed, 57 insertions, 5 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 1ac8fc1c..afa88a47 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -483,9 +483,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

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/dafny1/Answer b/Test/dafny1/Answer
index d96e12a5..d0eba7cb 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -59,6 +59,10 @@ 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

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/runtest.bat b/Test/dafny1/runtest.bat
index b6fc7f62..cab18ddb 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -18,7 +18,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