Added wellformedness checks to method specifications

6 files changed, 93 insertions, 5 deletions

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

+}