Dafny: added ensures clauses to functions

6 files changed, 216 insertions, 20 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 4b4bf920..34b9a0be 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -87,17 +87,17 @@ Execution trace:
     (0,0): anon0

 SmallTests.dfy(61,36): Error: possible division by zero

 Execution trace:

-    (0,0): anon10_Then

+    (0,0): anon12_Then

 SmallTests.dfy(62,51): Error: possible division by zero

 Execution trace:

-    (0,0): anon10_Else

+    (0,0): anon12_Else

     (0,0): anon3

-    (0,0): anon11_Else

+    (0,0): anon13_Else

 SmallTests.dfy(63,22): Error: target object may be null

 Execution trace:

-    (0,0): anon10_Then

+    (0,0): anon12_Then

     (0,0): anon3

-    (0,0): anon11_Then

+    (0,0): anon13_Then

     (0,0): anon6

 SmallTests.dfy(82,20): Error: decreases expression must be well defined at top of each loop iteration

 Execution trace:

@@ -129,7 +129,7 @@ Dafny program verifier finished with 28 verified, 9 errors
 -------------------- Definedness.dfy --------------------

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

 Execution trace:

-    (0,0): anon0

+    (0,0): anon3_Else

 Definedness.dfy(15,16): Error: possible division by zero

 Execution trace:

     (0,0): anon0

@@ -263,8 +263,22 @@ Execution trace:
 Definedness.dfy(210,23): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

+Definedness.dfy(231,30): Error: possible violation of function postcondition

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

+Definedness.dfy(238,22): Error: target object may be null

+Execution trace:

+    (0,0): anon5_Then

+    (0,0): anon2

+    (0,0): anon6_Then

+Definedness.dfy(254,24): Error: possible violation of function postcondition

+Execution trace:

+    (0,0): anon7_Then

+    (0,0): anon2

+    (0,0): anon8_Else

 

-Dafny program verifier finished with 21 verified, 29 errors

+Dafny program verifier finished with 23 verified, 32 errors

 

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

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

@@ -293,14 +307,14 @@ Execution trace:
     (0,0): anon0

 Array.dfy(107,6): Error: insufficient reads clause to read array element

 Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Then

-    (0,0): anon5_Then

+    (0,0): anon7_Else

+    (0,0): anon8_Then

+    (0,0): anon9_Then

 Array.dfy(115,6): Error: insufficient reads clause to read array element

 Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Then

-    (0,0): anon5_Then

+    (0,0): anon7_Else

+    (0,0): anon8_Then

+    (0,0): anon9_Then

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

 Execution trace:

     (0,0): anon0

@@ -348,7 +362,7 @@ Dafny program verifier finished with 16 verified, 2 errors
 -------------------- BadFunction.dfy --------------------

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

 Execution trace:

-    (0,0): anon0

+    (0,0): anon3_Else

 

 Dafny program verifier finished with 2 verified, 1 error

 

@@ -437,7 +451,7 @@ DTypes.dfy(54,18): Error: assertion violation
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 13 verified, 3 errors

+Dafny program verifier finished with 14 verified, 3 errors

 

 -------------------- TypeParameters.dfy --------------------

 TypeParameters.dfy(41,22): Error: assertion violation

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index c6f0737c..d925587b 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -74,3 +74,16 @@ class Node { }
 

 class CP<T,U> {

 }

+

+datatype Data {

+  Lemon;

+  Kiwi(int);

+}

+

+function G(d: Data): int

+  requires d != #Data.Lemon;

+{

+  match d

+  case Lemon => G(d)

+  case Kiwi(x) => 7

+}

diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index d557de21..1cb74b1d 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -213,3 +213,45 @@ class StatementTwoShoes {
     }

   }

 }

+

+// ----------------- function postconditions ----------------------

+

+class Mountain { var x: int; }

+

+function Postie0(c: Mountain): Mountain

+  requires c != null;

+  ensures Postie0(c) != null && Postie0(c).x <= Postie0(c).x;

+  ensures Postie0(c).x == Postie0(c).x;

+{

+  c

+}

+

+function Postie1(c: Mountain): Mountain

+  requires c != null;

+  ensures Postie1(c) != null && Postie1(c).x == 5;  // error: postcondition violation (but no well-formedness problem)

+{

+  c

+}

+

+function Postie2(c: Mountain): Mountain

+  requires c != null && c.x == 5;

+  ensures Postie2(c).x == 5;  // well-formedness error (null dereference)

+{

+  c

+}

+

+function Postie3(c: Mountain): Mountain  // all is cool

+  requires c != null && c.x == 5;

+  ensures Postie3(c) != null && Postie3(c).x < 10;

+  ensures Postie3(c).x == 5;

+{

+  c

+}

+

+function Postie4(c: Mountain): Mountain

+  requires c != null && c.x <= 5;

+  ensures Postie4(c) != null && Postie4(c).x < 10;

+  ensures Postie4(c).x == 5;  // error: postcondition might not hold

+{

+  c

+}

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index b8f9591f..5b51b3e4 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -9,7 +9,7 @@ Dafny program verifier finished with 22 verified, 0 errors
 

 -------------------- PriorityQueue.dfy --------------------

 

-Dafny program verifier finished with 12 verified, 0 errors

+Dafny program verifier finished with 24 verified, 0 errors

 

 -------------------- BinaryTree.dfy --------------------

 

diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index 76e4b1d6..4a9ba220 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -49,7 +49,7 @@ class PriorityQueue {
     requires 1 <= k && k <= n;

     requires MostlyValid();

     requires (forall j :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);

-    requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j != k ==> a[j/2/2] <= a[j]);

+    requires (forall j :: 1 <= j && j <= n ==> j/2 != k);  // k is a child

     modifies a;

     ensures Valid();

   {

@@ -58,7 +58,7 @@ class PriorityQueue {
     while (1 < i)

       invariant i <= k && MostlyValid();

       invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);

-      invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j != i ==> a[j/2/2] <= a[j]);

+      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

     {

       if (a[i/2] <= a[i]) {

         return;

@@ -84,7 +84,7 @@ class PriorityQueue {
     requires 1 <= k;

     requires MostlyValid();

     requires (forall j :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);

-    requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);

+    requires k == 1;

     modifies a;

     ensures Valid();

   {

@@ -92,7 +92,121 @@ class PriorityQueue {
     while (2*i <= n)  // while i is not a leaf

       invariant 1 <= i && MostlyValid();

       invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);

-      invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);

+      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

+    {

+      var smallestChild;

+      if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {

+        smallestChild := 2*i + 1;

+      } else {

+        smallestChild := 2*i;

+      }

+      if (a[i] <= a[smallestChild]) {

+        return;

+      }

+      var tmp := a[i];  a[i] := a[smallestChild];  a[smallestChild] := tmp;

+      i := smallestChild;

+      assert 1 <= i/2/2 ==> a[i/2/2] <= a[i];

+    }

+  }

+}

+

+// ---------- Alternative specifications ----------

+

+class PriorityQueue_Alternative {

+  var N: int;  // capacity

+  var n: int;  // current size

+  ghost var Repr: set<object>;  // set of objects that make up the representation of a PriorityQueue

+

+  var a: array<int>;  // private implementation of PriorityQueu

+

+  function Valid(): bool

+    reads this, Repr;

+  {

+    MostlyValid() &&

+    (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])

+  }

+

+  function MostlyValid(): bool

+    reads this, Repr;

+  {

+    this in Repr && a in Repr &&

+    a != null && a.Length == N+1 &&

+    0 <= n && n <= N

+  }

+

+  method Init(capacity: int)

+    requires 0 <= capacity;

+    modifies this;

+    ensures Valid() && fresh(Repr - {this});

+    ensures N == capacity;

+  {

+    N := capacity;

+    var arr := new int[N+1];

+    a := arr;

+    n := 0;

+    Repr := {this};

+    Repr := Repr + {a};

+  }

+

+  method Insert(x: int)

+    requires Valid() && n < N;

+    modifies this, a;

+    ensures Valid() && fresh(Repr - old(Repr));

+    ensures n == old(n) + 1 && N == old(N);

+  {

+    n := n + 1;

+    a[n] := x;

+    call SiftUp(n);

+  }

+

+  method SiftUp(k: int)

+    requires 1 <= k && k <= n;

+    requires MostlyValid();

+    requires (forall j :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);

+    requires (forall j :: 1 <= j && j <= n ==> j/2 != k);  // k is a child

+    modifies a;

+    ensures Valid();

+  {

+    var i := k;

+    assert MostlyValid();

+    while (1 < i)

+      invariant i <= k && MostlyValid();

+      invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);

+      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

+    {

+      if (a[i/2] <= a[i]) {

+        return;

+      }

+      var tmp := a[i];  a[i] := a[i/2];  a[i/2] := tmp;

+      i := i / 2;

+    }

+  }

+

+  method RemoveMin() returns (x: int)

+    requires Valid() && 1 <= n;

+    modifies this, a;

+    ensures Valid() && fresh(Repr - old(Repr));

+    ensures n == old(n) - 1;

+  {

+    x := a[1];

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

+    n := n - 1;

+    call SiftDown(1);

+  }

+

+  method SiftDown(k: int)

+    requires 1 <= k;

+    requires MostlyValid();

+    requires (forall j :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);

+    requires k == 1;  // k is the root

+    modifies a;

+    ensures Valid();

+  {

+    var i := k;

+    while (2*i <= n)  // while i is not a leaf

+      invariant 1 <= i && MostlyValid();

+      invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);

+      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

     {

       var smallestChild;

       if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {

diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy
index fb530258..76925e8e 100644
--- a/Test/dafny1/TerminationDemos.dfy
+++ b/Test/dafny1/TerminationDemos.dfy
@@ -30,6 +30,19 @@ class Ackermann {
     else

       F(m - 1, F(m, n - 1))

   }

+/*

+  function G(m: int, n: int): int

+    requires 0 <= m && 0 <= n;

+    ensures 0 <= G(m, n);

+  {

+    if m == 0 then

+      n + 1

+    else if n == 0 then

+      G(m - 1, 1)

+    else

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

+  }

+*/

 }

 

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