Dafny:

* Improved design and implementation of SplitExpr
* Fixed some tests in dafny0/Use.dfy
* Added test case (in dafny0/Termination.dfy) to test the recent strengthening of set axioms

5 files changed, 109 insertions, 22 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 7456ffaa..34b15b8a 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -372,7 +372,7 @@ Execution trace:
     Termination.dfy(119,16): anon9_Else

     (0,0): anon5

 

-Dafny program verifier finished with 22 verified, 4 errors

+Dafny program verifier finished with 23 verified, 4 errors

 

 -------------------- Use.dfy --------------------

 Use.dfy(16,18): Error: assertion violation

@@ -393,17 +393,20 @@ Execution trace:
 Use.dfy(126,23): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(138,5): Error: assertion violation

+Use.dfy(143,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(138,5): Error: assertion violation

+Use.dfy(143,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(208,19): Error: assertion violation

+Use.dfy(143,5): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Use.dfy(213,19): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 39 verified, 9 errors

+Dafny program verifier finished with 39 verified, 10 errors

 

 -------------------- DTypes.dfy --------------------

 DTypes.dfy(15,14): Error: assertion violation

@@ -440,3 +443,7 @@ Dafny program verifier finished with 27 verified, 4 errors
 -------------------- Datatypes.dfy --------------------

 

 Dafny program verifier finished with 10 verified, 0 errors

+

+-------------------- SplitExpr.dfy --------------------

+

+Dafny program verifier finished with 5 verified, 0 errors

diff --git a/Test/dafny0/SplitExpr.dfy b/Test/dafny0/SplitExpr.dfy
new file mode 100644
index 00000000..80b67c10
--- /dev/null
+++ b/Test/dafny0/SplitExpr.dfy
@@ -0,0 +1,56 @@
+class UnboundedStack<T> {

+  var top: Node<T>;

+  ghost var footprint: set<object>;

+  ghost var content: seq<T>; 

+

+  function IsUnboundedStack(): bool

+    reads {this} + footprint;

+  {

+    this in footprint &&

+    (top == null  ==>  content == []) &&

+    (top != null  ==>  top in footprint && top.footprint <= footprint &&

+                       top.prev == null && content == top.content && top.Valid())

+  }

+

+  function IsEmpty(): bool

+    reads {this};

+  { content == [] }

+

+  method Pop() returns (result: T)

+    requires IsUnboundedStack() && !IsEmpty();

+    modifies footprint;

+    ensures IsUnboundedStack() && content == old(content)[1..];

+  {

+    result := top.val;

+    // The following assert does the trick, because it gets inlined and thus

+    // exposes top.next.Valid() (if top.next != null):

+    footprint := footprint - top.footprint;  top := top.next;

+    // In a previous version of the implementation of the SplitExpr transformation, the

+    // following assert did not have the intended effect of being used as a lemma:

+    assert top != null ==> top.Valid();

+    if (top != null) {

+      footprint := footprint + top.footprint;  top.prev := null;

+    }

+    content := content[1..];

+} }

+

+class Node<T> {

+  var val: T;  

+  var next: Node<T>;

+  var prev: Node<T>;

+  var footprint: set<Node<T>>;

+  var content: seq<T>;

+

+  function Valid(): bool

+    reads this, footprint;

+  {

+    this in footprint && !(null in footprint) &&

+    (next == null  ==>  content == [val])  &&

+    (next != null  ==>  next in footprint &&

+                        next.footprint < footprint &&

+                        !(this in next.footprint) &&

+                        next.prev == this &&

+                        content == [val] + next.content &&

+                        next.Valid())

+  }

+}

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 27004653..974dadab 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -151,3 +151,22 @@ method FailureToProveTermination5(b: bool, N: int)
     n := n + 1;

   }

 }

+

+class Node {

+  var next: Node;

+  var footprint: set<Node>;

+

+  function Valid(): bool

+    reads this, footprint;

+    // In a previous (and weaker) axiomatization of sets, there had been two problems

+    // with trying to prove the termination of this function.  First, the default

+    // decreases clause (derived from the reads clause) had been done incorrectly for

+    // a list of expressions.  Second, the set axiomatization had not been strong enough.

+  {

+    this in footprint && !(null in footprint) &&

+    (next != null  ==>  next in footprint &&

+                        next.footprint < footprint &&

+                        this !in next.footprint &&

+                        next.Valid())

+  }

+}

diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy
index 20928f41..7a963382 100644
--- a/Test/dafny0/Use.dfy
+++ b/Test/dafny0/Use.dfy
@@ -128,50 +128,55 @@ class T {
   }

 

   function K(): bool

-    reads this; decreases false;

+    reads this; decreases 0;

   {

-    x <= 100 || (1 < 0 && KK())

+    x <= 100 || (1 < 0 && KKK())

   }

-  unlimited function KK(): bool

-    reads this; decreases true;

+  function KK(): bool

+    reads this; decreases 1;

   {

     K()

   }

+  unlimited function KKK(): bool

+    reads this; decreases 2;

+  {

+    KK()

+  }

 

   method R0()

-    requires KK();

+    requires KKK();  // this expands to both KKK() and KK(); the def. of KK() expands to K#limited

     modifies this;

   {

     x := x - 1;

-    assert KK();  // error (does not know exact definition of K from the initial state)

+    assert KKK();  // error (does not know exact definition of K from the initial state)

   }

 

   method R1()

-    requires KK();

+    requires KKK();  // this expands to both KKK() and KK(); the def. of KK() expands to K#limited

     modifies this;

   {

-    use K();  // KK in the precondition and KK's definition give K#limited, which this use expands

+    use K();  // this equates K#limited and K, so the exact value of K() in the pre-state is now known

     x := x - 1;

-    assert KK();  // the assert expands KK to K, definition of K expands K

+    assert KKK();  // error: the assert expands KKK to KK, definition of KK expands K#limited (but not to K)

   }

 

   method R2()

-    requires KK();

+    requires KKK();  // this expands to both KKK() and KK(); the def. of KK() expands to K#limited (but not K)

     modifies this;

   {

     x := x - 1;

-    use K();

-    assert KK();  // error (does not know exact definition of K in the pre-state)

+    use K();  // this equates K#limited and K in the present state

+    assert KKK();  // error: the connection with the pre-state K is not known

   }

 

   method R3()

-    requires KK();

+    requires KKK();  // this expands to both KKK() and KK(); the def. of KK() expands to K#limited (but not K)

     modifies this;

   {

-    use K();

+    use K();  // this equates K#limited and K, so the pre-state K() is known

     x := x - 1;

-    use K();

-    assert KK();  // thar it is

+    use K();  // this equates K#limited and K in the present state

+    assert KKK();  // thar it is:  this expands to both KKK and KK, and the def. of KK expands to K#limited

   }

 }

 

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index aa45ca05..0e8146c0 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -14,7 +14,7 @@ for %%f in (Simple.dfy) do (
 for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

             Termination.dfy Use.dfy DTypes.dfy

-            TypeParameters.dfy Datatypes.dfy) do (

+            TypeParameters.dfy Datatypes.dfy SplitExpr.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 %* %%f