Dafny: updated test files (will soon update Answer files as well)

2 files changed, 92 insertions, 27 deletions

diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy
index 76e67205..c92dd065 100644
--- a/Test/dafny1/FindZero.dfy
+++ b/Test/dafny1/FindZero.dfy
@@ -1,12 +1,12 @@
 method FindZero(a: array<int>) returns (r: int)

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

+  requires a != null && forall i :: 0 <= 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;

+  ensures r < 0 ==> forall i :: 0 <= 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;

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

   {

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

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

@@ -16,11 +16,11 @@ method FindZero(a: array<int>) returns (r: int)
 }

 

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

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

+  requires a != null && forall i :: 0 <= 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;

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

   decreases m;

 {

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

@@ -28,3 +28,49 @@ ghost method Lemma(a: array<int>, k: int, m: int)
     Lemma(a, k+1, m-1);

   }

 }

+

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

+

+method FindZero_GhostLoop(a: array<int>) returns (r: int)

+  requires a != null && forall i :: 0 <= 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 < a.Length ==> a[i] != 0;

+{

+  var n := 0;

+  while (n < a.Length)

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

+  {

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

+    ghost var m := n;

+    while (m < n + a[n])

+      invariant m <= n + a[n] && m < a.Length;

+      invariant n + a[n] - m <= a[m];

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

+    {

+      m := m + 1;

+      if (m == a.Length) { break; }

+    }

+    n := n + a[n];

+  }

+  return -1;

+}

+

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

+

+method FindZero_Assert(a: array<int>) returns (r: int)

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

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

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

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

+{

+  var n := 0;

+  while (n < a.Length)

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

+  {

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

+    assert forall m {:induction} :: n <= m < n + a[n] && m < a.Length ==> n+a[n]-m <= a[m];

+    n := n + a[n];

+  }

+  return -1;

+}

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 5fd87a6c..6f6a7ba7 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -157,45 +157,45 @@ function last(xs: List): Nat
     case Cons(z, zs) => last(ys)

 }

 

-function mapF(xs: List): List

+function map(f: FunctionValue, xs: List): List

 {

   match xs

   case Nil => Nil

-  case Cons(y, ys) => Cons(HardcodedUninterpretedFunction(y), mapF(ys))

+  case Cons(y, ys) => Cons(Apply(f, y), map(f, ys))

 }

-function HardcodedUninterpretedFunction(n: Nat): Nat

 

-function takeWhileAlways(hardcodedResultOfP: Bool, xs: List): List

+// In the following two functions, parameter "p" stands for a predicate:  applying p and

+// getting Zero means "false" and getting anything else means "true".

+

+function takeWhileAlways(p: FunctionValue, xs: List): List

 {

   match xs

   case Nil => Nil

   case Cons(y, ys) =>

-    if whilePredicate(hardcodedResultOfP, y) == True

-    then Cons(y, takeWhileAlways(hardcodedResultOfP, ys))

+    if Apply(p, y) != Zero

+    then Cons(y, takeWhileAlways(p, ys))

     else Nil

 }

-function whilePredicate(result: Bool, arg: Nat): Bool { result }

 

-function dropWhileAlways(hardcodedResultOfP: Bool, xs: List): List

+function dropWhileAlways(p: FunctionValue, xs: List): List

 {

   match xs

   case Nil => Nil

   case Cons(y, ys) =>

-    if whilePredicate(hardcodedResultOfP, y) == True

-    then dropWhileAlways(hardcodedResultOfP, ys)

+    if Apply(p, y) != Zero

+    then dropWhileAlways(p, ys)

     else Cons(y, ys)

 }

 

-function filterP(xs: List): List

+function filter(p: FunctionValue, xs: List): List

 {

   match xs

   case Nil => Nil

   case Cons(y, ys) =>

-    if HardcodedUninterpretedPredicate(y) == True

-    then Cons(y, filterP(ys))

-    else filterP(ys)

+    if Apply(p, y) != Zero

+    then Cons(y, filter(p, ys))

+    else filter(p, ys)

 }

-function HardcodedUninterpretedPredicate(n: Nat): Bool

 

 function insort(n: Nat, xs: List): List

 {

@@ -275,7 +275,27 @@ function mirror(t: Tree): Tree
   case Node(l, x, r) => Node(mirror(r), x, mirror(l))

 }

 

+// Function parameters

+

+// Dafny currently does not support passing functions as arguments.  To simulate

+// arbitrary functions, the following type (declared as a class) and Apply function

+// play the role of applying some prescribed function (here, an instance of the class)

+// to some argument.

+

+class FunctionValue { }

+function Apply(f: FunctionValue, x: Nat): Nat  // this function is left uninterpreted

+

+// The following functions stand for the constant "false" and "true" functions,

+// respectively.

+

+function AlwaysFalseFunction(): FunctionValue

+  ensures forall n :: Apply(AlwaysFalseFunction(), n) == Zero;

+function AlwaysTrueFunction(): FunctionValue

+  ensures forall n :: Apply(AlwaysTrueFunction(), n) != Zero;

+

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

 // The theorems to be proved

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

 

 ghost method P1()

   ensures (forall n, xs :: concat(take(n, xs), drop(n, xs)) == xs);

@@ -335,7 +355,7 @@ ghost method P11()
 }

 

 ghost method P12()

-  ensures (forall n, xs :: drop(n, mapF(xs)) == mapF(drop(n, xs)));

+  ensures (forall n, xs, f :: drop(n, map(f, xs)) == map(f, drop(n, xs)));

 {

 }

 

@@ -345,7 +365,7 @@ ghost method P13()
 }

 

 ghost method P14()

-  ensures (forall xs, ys :: filterP(concat(xs, ys)) == concat(filterP(xs), filterP(ys)));

+  ensures (forall xs, ys, p :: filter(p, concat(xs, ys)) == concat(filter(p, xs), filter(p, ys)));

 {

 }

 

@@ -456,12 +476,12 @@ ghost method P34()
 }

 

 ghost method P35()

-  ensures (forall xs :: dropWhileAlways(False, xs) == xs);

+  ensures (forall xs :: dropWhileAlways(AlwaysFalseFunction(), xs) == xs);

 {

 }

 

 ghost method P36()

-  ensures (forall xs :: takeWhileAlways(True, xs) == xs);

+  ensures (forall xs :: takeWhileAlways(AlwaysTrueFunction(), xs) == xs);

 {

 }

 

@@ -487,7 +507,7 @@ ghost method P40()
 }

 

 ghost method P41()

-  ensures (forall n, xs :: take(n, mapF(xs)) == mapF(take(n, xs)));

+  ensures (forall n, xs, f :: take(n, map(f, xs)) == map(f, take(n, xs)));

 {

 }

 

@@ -496,8 +516,7 @@ ghost method P42()
 {

 }

 

-ghost method P43(p: Bool)

-  // this is an approximation of the actual problem 43

+ghost method P43(p: FunctionValue)

   ensures (forall xs :: concat(takeWhileAlways(p, xs), dropWhileAlways(p, xs)) == xs);

 {

 }