Added wellformedness checks to method specifications

11 files changed, 110 insertions, 17 deletions

diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer
index 954ca3b0..a0ae9d01 100644
--- a/Test/VSI-Benchmarks/Answer
+++ b/Test/VSI-Benchmarks/Answer
@@ -1,32 +1,32 @@
 

 -------------------- b1.dfy --------------------

 

-Dafny program verifier finished with 2 verified, 0 errors

+Dafny program verifier finished with 4 verified, 0 errors

 

 -------------------- b2.dfy --------------------

 

-Dafny program verifier finished with 3 verified, 0 errors

+Dafny program verifier finished with 6 verified, 0 errors

 

 -------------------- b3.dfy --------------------

 

-Dafny program verifier finished with 5 verified, 0 errors

+Dafny program verifier finished with 10 verified, 0 errors

 

 -------------------- b4.dfy --------------------

 

-Dafny program verifier finished with 6 verified, 0 errors

+Dafny program verifier finished with 11 verified, 0 errors

 

 -------------------- b5.dfy --------------------

 

-Dafny program verifier finished with 12 verified, 0 errors

+Dafny program verifier finished with 22 verified, 0 errors

 

 -------------------- b6.dfy --------------------

 

-Dafny program verifier finished with 12 verified, 0 errors

+Dafny program verifier finished with 21 verified, 0 errors

 

 -------------------- b7.dfy --------------------

 

-Dafny program verifier finished with 11 verified, 0 errors

+Dafny program verifier finished with 23 verified, 0 errors

 

 -------------------- b8.dfy --------------------

 

-Dafny program verifier finished with 22 verified, 0 errors

+Dafny program verifier finished with 42 verified, 0 errors

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 6c0cfe81..457bc894 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -54,6 +54,7 @@ class Array {
   method Set(i: int, x: int);

     requires 0 <= i && i < |contents|;

     modifies this;

+    ensures |contents| == |old(contents)|;

     ensures contents[..i] == old(contents[..i]);

     ensures contents[i] == x;

     ensures contents[i+1..] == old(contents[i+1..]);

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index 3fa80b4c..ab1285f6 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -43,7 +43,8 @@ class Map<Key,Value> {
     requires Valid();

     modifies this;

     ensures Valid();

-    ensures (forall i :: 0 <= i && i < |keys| && old(keys)[i] == key ==>

+    ensures (forall i :: 0 <= i && i < |old(keys)| && old(keys)[i] == key ==>

+              |keys| == |old(keys)| &&

               keys[i] == key && values[i] == val &&

               (forall j :: 0 <= j && j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j]));

     ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val];

@@ -69,7 +70,7 @@ class Map<Key,Value> {
     // other values don't change:

     ensures key !in old(keys) ==> keys == old(keys) && values == old(values);

     ensures key in old(keys) ==>

-            key !in keys &&

+            |keys| == |old(keys)| - 1 && key !in keys &&

             (exists h ::

               0 <= h && h <= |keys| &&

               keys[..h] == old(keys)[..h] &&

diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy
index 34ff5f57..2e274845 100644
--- a/Test/VSI-Benchmarks/b5.dfy
+++ b/Test/VSI-Benchmarks/b5.dfy
@@ -109,6 +109,7 @@ class Queue<T> {
     requires 0 < |contents|;

     modifies footprint;

     ensures Valid() && fresh(footprint - old(footprint));

+    ensures |contents| == |old(contents)|;

     ensures (exists i :: 0 <= i && i <= |contents| &&

               contents == old(contents)[i..] + old(contents)[..i]);

   {

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index a0cb6e74..fec36c29 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -34,6 +34,7 @@ class Glossary {
     ensures r != null && fresh(r);

     ensures |r.contents| == |old(q.contents)|;

     ensures (forall i, j :: 0 <= i && i < j && j < |r.contents| ==>

+                r.Get(i) != null &&

                 r.Get(i).AtMost(r.Get(j)));

     //perm is a permutation

     ensures |perm| == |r.contents|; // ==|pperm|

@@ -289,7 +290,8 @@ class Map<Key,Value> {
     requires Valid();

     modifies this;

     ensures Valid();

-    ensures (forall i :: 0 <= i && i < |keys| && old(keys)[i] == key ==>

+    ensures (forall i :: 0 <= i && i < |old(keys)| && old(keys)[i] == key ==>

+              |keys| == |old(keys)| &&

               keys[i] == key && values[i] == val &&

               (forall j :: 0 <= j && j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j]));

     ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val];

@@ -315,7 +317,7 @@ class Map<Key,Value> {
     // other values don't change:

     ensures key !in old(keys) ==> keys == old(keys) && values == old(values);

     ensures key in old(keys) ==>

-            key !in keys &&

+            |keys| == |old(keys)| - 1 && key !in keys &&

             (exists h ::

               0 <= h && h <= |keys| &&

               keys[..h] == old(keys)[..h] &&

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index d46dc7fe..a364d4e9 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -116,8 +116,33 @@ Execution trace:
     (0,0): anon0

     (0,0): anon4_Else

     (0,0): anon3

+SmallTests.dfy(162,7): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(169,16): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(178,16): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(179,21): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+SmallTests.dfy(180,17): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(187,16): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(204,18): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(209,18): Error: target object may be null

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 10 verified, 8 errors

+Dafny program verifier finished with 30 verified, 16 errors

 

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

 

diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy
index 8492f217..2b3168b2 100644
--- a/Test/dafny0/Datatypes.dfy
+++ b/Test/dafny0/Datatypes.dfy
@@ -26,7 +26,7 @@ class Node {
 

   method Add(d: int, L: List<int>) returns (r: Node)

     requires Repr(L);

-    ensures r.Repr(#List.Cons(d, L));

+    ensures r != null && r.Repr(#List.Cons(d, L));

   {

     r := new Node;

     r.data := d;

diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy
index 952c47d2..07dc2f7e 100644
--- a/Test/dafny0/ListContents.dfy
+++ b/Test/dafny0/ListContents.dfy
@@ -39,7 +39,7 @@ class Node<T> {
 

   method Prepend(d: T) returns (r: Node<T>)

     requires Valid();

-    ensures r.Valid() && fresh(r.footprint - old(footprint));

+    ensures r != null && r.Valid() && fresh(r.footprint - old(footprint));

     ensures r.list == [d] + list;

   {

     r := new Node<T>;

diff --git a/Test/dafny0/Queue.dfy b/Test/dafny0/Queue.dfy
index da1ab2c5..a87bfc0d 100644
--- a/Test/dafny0/Queue.dfy
+++ b/Test/dafny0/Queue.dfy
@@ -59,6 +59,7 @@ class Queue<T> {
     requires 0 < |contents|;

     modifies footprint;

     ensures Valid() && fresh(footprint - old(footprint));

+    ensures |contents| == |old(contents)|;

     ensures (exists i :: 0 <= i && i <= |contents| &&

               contents == old(contents)[i..] + old(contents)[..i]);

   {

diff --git a/Test/dafny0/SchorrWaite.dfy b/Test/dafny0/SchorrWaite.dfy
index 527d379f..fb06d211 100644
--- a/Test/dafny0/SchorrWaite.dfy
+++ b/Test/dafny0/SchorrWaite.dfy
@@ -42,7 +42,7 @@ class Main {
     ensures (forall n :: n in S && n.marked ==>

                 n in stackNodes ||

                 (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));

-    ensures (forall n: Node :: old(n.marked) ==> n.marked);

+    ensures (forall n: Node :: n in S && old(n.marked) ==> n.marked);

     ensures (forall n :: n in S ==>

                 n.childrenVisited == old(n.childrenVisited) &&

                 n.children == old(n.children));

@@ -58,7 +58,7 @@ class Main {
                 (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));

         invariant (forall j :: 0 <= j && j < i ==>

                     root.children[j] == null || root.children[j].marked);

-        invariant (forall n: Node :: old(n.marked) ==> n.marked);

+        invariant (forall n: Node :: n in S && old(n.marked) ==> n.marked);

         invariant (forall n :: n in S ==>

                 n.childrenVisited == old(n.childrenVisited) &&

                 n.children == old(n.children));

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 3a2ca13c..3e626f25 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -151,3 +151,65 @@ class Modifies {
     }

   }

 }

+

+// ----------------- wellformed specifications ----------------------

+

+class SoWellformed {

+  var xyz: int;

+  var next: SoWellformed;

+

+  function F(x: int): int

+  { 5 / x }  // error: possible division by zero

+

+  function G(x: int): int

+    requires 0 < x;

+  { 5 / x }

+

+  function H(x: int): int

+    decreases 5/x;  // error: possible division by zero

+  { 12 }

+

+  function I(x: int): int

+    requires 0 < x;

+    decreases 5/x;

+  { 12 }

+

+  method M(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

+    requires a.xyz == 7;  // error: not always defined

+    ensures c ==> d.xyz == -7;  // error: not always defined

+    decreases 5 / b;  // error: not always defined

+  {

+    c := false;

+  }

+

+  method N(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

+    decreases 5 / b;

+    requires a.next != null;  // error: not always defined

+    requires a.next.xyz == 7;  // this is well-defined, given that the previous line is

+    requires b < -2;

+    ensures 0 <= b ==> d.xyz == -7 && !c;

+  {

+    c := true;

+  }

+

+  method O(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

+    modifies a.next;  // this may not be well-defined, but that's okay for modifies clauses

+  {

+    c := true;

+  }

+

+  method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed);

+    requires next != null;

+    modifies this;

+    ensures next.xyz < 100;  // error: may not be well-defined (if body sets next to null)

+

+  method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);

+    requires next != null;

+    modifies s;

+    ensures next.xyz < 100;  // error: may not be well-defined (if this in s and body sets next to null)

+

+  method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);

+    requires next != null && this !in s;

+    modifies s;

+    ensures next.xyz < 100;  // fine

+}