Dafny:

* Allow ghost methods (all "ghost" keywords are currently parsed and then ignored)
* Improved and made more automatic the treatment of "use" functions (a good next step would be to automatically infer which functions would make good "use" functions)
* Include preconditions in all definedness checks of function-call expressions

5 files changed, 412 insertions, 16 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index d1584333..107cab0b 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -134,17 +134,35 @@ Dafny program verifier finished with 6 verified, 0 errors
 Dafny program verifier finished with 6 verified, 0 errors

 

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

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

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

 Execution trace:

     (0,0): anon0

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

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

 Execution trace:

     (0,0): anon0

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

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

+Execution trace:

+    (0,0): anon0

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

+Execution trace:

+    (0,0): anon0

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

+Execution trace:

+    (0,0): anon0

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

+Execution trace:

+    (0,0): anon0

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

+Execution trace:

+    (0,0): anon0

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

+Execution trace:

+    (0,0): anon0

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

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 6 verified, 3 errors

+Dafny program verifier finished with 20 verified, 9 errors

 

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

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

@@ -172,3 +190,11 @@ Dafny program verifier finished with 10 verified, 2 errors
 -------------------- Datatypes.dfy --------------------

 

 Dafny program verifier finished with 6 verified, 0 errors

+

+-------------------- UnboundedStack.dfy --------------------

+

+Dafny program verifier finished with 7 verified, 0 errors

+

+-------------------- SumOfCubes.dfy --------------------

+

+Dafny program verifier finished with 10 verified, 0 errors

diff --git a/Test/dafny0/SumOfCubes.dfy b/Test/dafny0/SumOfCubes.dfy
new file mode 100644
index 00000000..389c885c
--- /dev/null
+++ b/Test/dafny0/SumOfCubes.dfy
@@ -0,0 +1,110 @@
+class SumOfCubes {

+  class use function SumEmUp(n: int, m: int): int

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

+    decreases m - n;

+  {

+    if m == n then 0 else n*n*n + SumEmUp(n+1, m)

+  }

+

+  class method Socu(n: int, m: int) returns (r: int)

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

+    ensures r == SumEmUp(n, m);

+  {

+    call a := SocuFromZero(m);

+    call b := SocuFromZero(n);

+    r := a - b;

+    call Lemma0(n, m);

+  }

+

+  class method SocuFromZero(k: int) returns (r: int)

+    requires 0 <= k;

+    ensures r == SumEmUp(0, k);

+  {

+    call g := Gauss(k);

+    r := g * g;

+    call Lemma1(k);

+  }

+

+  ghost class method Lemma0(n: int, m: int)

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

+    ensures SumEmUp(n, m) == SumEmUp(0, m) - SumEmUp(0, n);

+  {

+    var k := n;

+    while (k < m) 

+      invariant n <= k && k <= m;

+      invariant SumEmDown(0, n) + SumEmDown(n, k) == SumEmDown(0, k);

+      decreases m - k;

+    {

+      k := k + 1;

+    }

+    call Lemma3(0, n);

+    call Lemma3(n, k);

+    call Lemma3(0, k);

+  }

+

+  class use function GSum(k: int): int

+    requires 0 <= k;

+    decreases k;

+  {

+    if k == 0 then 0 else GSum(k-1) + k-1

+  }

+

+  ghost class method Gauss(k: int) returns (r: int)

+    requires 0 <= k;

+    ensures r == GSum(k);

+  {

+    r := k * (k - 1) / 2;

+    call Lemma2(k);

+  }

+

+  ghost class method Lemma1(k: int)

+    requires 0 <= k;

+    ensures SumEmUp(0, k) == GSum(k) * GSum(k);

+  {

+    var i := 0;

+    while (i < k)

+      invariant i <= k;

+      invariant SumEmDown(0, i) == GSum(i) * GSum(i);

+      decreases k - i;

+    {

+      call Lemma2(i);

+      i := i + 1;

+    }

+    call Lemma3(0, k);

+  }

+

+  ghost class method Lemma2(k: int)

+    requires 0 <= k;

+    ensures 2 * GSum(k) == k * (k - 1);

+  {

+    var i := 0;

+    while (i < k)

+      invariant i <= k;

+      invariant 2 * GSum(i) == i * (i - 1);

+      decreases k - i;

+    {

+      i := i + 1;

+    }

+  }

+

+  class use function SumEmDown(n: int, m: int): int

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

+    decreases m;

+  {

+    if m == n then 0 else SumEmDown(n, m-1) + (m-1)*(m-1)*(m-1)

+  }

+

+  ghost class method Lemma3(n: int, m: int)

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

+    ensures SumEmUp(n, m) == SumEmDown(n, m);

+  {

+    var k := n;

+    while (k < m)

+      invariant n <= k && k <= m;

+      invariant SumEmUp(n, m) == SumEmDown(n, k) + SumEmUp(k, m);

+      decreases m - k;

+    {

+      k := k + 1;

+    }

+  }

+}

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

+  ghost var representation: set<object>;

+  ghost var content: seq<T>;

+  var top: Node<T>;

+

+  function IsUnboundedStack(): bool

+    reads this, representation;

+  {

+    this in representation &&

+    (top == null ==>

+      content == []) &&

+    (top != null ==>

+      top in representation && this !in top.footprint && top.footprint <= representation &&

+      content == top.content &&

+      top.Valid())

+  }

+

+  method InitUnboundedStack()

+    modifies this;

+    ensures IsUnboundedStack();

+    ensures content == [];

+  {

+    this.top := null;

+    this.content := [];

+    this.representation := {this};

+  }

+

+  method Push(val: T)

+    requires IsUnboundedStack();

+    modifies this;

+    ensures IsUnboundedStack();

+    ensures content == [val] + old(content);

+  {

+    var tmp := new Node<T>;

+    call tmp.InitNode(val,top);

+    top := tmp;

+    representation := representation + top.footprint;

+    content := [val] + content;

+  }

+

+  method Pop() returns (result: T)

+    requires IsUnboundedStack();

+    requires content != [];

+    modifies this;

+    ensures IsUnboundedStack();

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

+  {

+    result := top.val;

+    top := top.next;

+    content := content[1..];

+  }

+

+  method isEmpty() returns (result: bool)

+    requires IsUnboundedStack();

+    ensures result <==> content == [];

+  {

+    result := top == null;

+  }

+}

+

+class Node<T> {

+  ghost var footprint: set<object>;

+  ghost var content: seq<T>;

+  var val: T;

+  var next: Node<T>;

+

+  function Valid(): bool

+    reads this, footprint;

+  {

+    this in footprint &&

+    (next == null ==>

+      content == [val]) &&

+    (next != null ==>

+      next in footprint && next.footprint <= footprint && this !in next.footprint &&

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

+      next.Valid())

+  }

+

+  method InitNode(val: T, next: Node<T>)

+    requires next != null ==> next.Valid() && !(this in next.footprint);

+    modifies this;

+    ensures Valid();

+    ensures next != null ==> content == [val] + next.content && 

+                             footprint == {this} + next.footprint;

+    ensures next == null ==> content == [val] &&

+                             footprint == {this};

+  {

+    this.val := val;

+    this.next := next;

+    if (next == null) {

+      this.footprint := {this};

+      this.content := [val];      

+    } else {

+      this.footprint := {this} + next.footprint;

+      this.content := [val] + next.content;      

+    }

+  }

+}

diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy
index 8b7eafc1..e006823e 100644
--- a/Test/dafny0/Use.dfy
+++ b/Test/dafny0/Use.dfy
@@ -1,7 +1,9 @@
 class T {

   var x: int;

 

-  use function F(y: int): int {

+  use function F(y: int): int

+    decreases 0;

+  {

     2*y

   }

 

@@ -9,37 +11,73 @@ class T {
     use F(4);

     use F(5);

     assert F(5) == 10;

-    assert F(7) == 14;  // error (definition not engaged)

+    assert F(7) == 14;

+    assert F(72) == 14;  // error (just plain wrong)

+  }

+

+  use function FF(y: int): int

+    decreases 1;

+  {

+    F(y)

+  }

+

+  method MM() {

+    assert F(5) == 10;

+    assert FF(6) == 12;  // error (definition of F not engaged)

+

+    assert F(7) == 14;

+    assert FF(7) == 14;  // now the inner definition of F has already been engaged

+

+    use F(8);

+    assert FF(8) == 16;  // same here

+

+    use FF(9);

+    assert FF(9) == 18;  // error (definition of F not engaged; the use of FF does not help)

   }

 

-  use function G(y: int): bool {

+  use function G(y: int): bool

+    decreases 0;

+  {

     0 <= y

   }

+  use function GG(y: int): bool

+    decreases 1;

+  {

+    G(y)

+  }

 

   method N(s: set<T>) {

     use G(4);

     use G(5);

     use G(-5);

-    assert G(5);

-    assert !G(-5);

-    assert G(7);  // error (definition not engaged)

+    assert GG(5);

+    assert !GG(-5);

+    assert GG(7);  // fine (the assert expands GG to G, then the definition of G kicks in)

+    assert !GG(-7);  // error (the negation disables the expansion of GG in the assert)

   }

 

   use function H(): int

     reads this;

+    decreases 0;

   {

     x

   }

+  use function HH(): int

+    reads this;

+    decreases 1;

+  {

+    H()

+  }

 

   method Q0()

     modifies this;

   {

     var t := x;

     use H();

-    assert H() == t;

+    assert HH() == t;

 

     x := x + 1;

-    assert old(H()) == t;

+    assert old(HH()) == t;

   }

 

   method Q1()

@@ -47,7 +85,7 @@ class T {
   {

     x := x + 1;

     use H();

-    assert H() == old(H()) + 1;  // error: does not know what old(H()) is

+    assert HH() == old(HH()) + 1;  // error: does not know what old(H()) is

   }

 

   method Q2()

@@ -56,7 +94,7 @@ class T {
     use H();

     x := x + 1;

     use H();

-    assert H() == old(H()) + 1;

+    assert HH() == old(HH()) + 1;

   }

 

   method Q3()

@@ -65,6 +103,129 @@ class T {
     x := x + 1;

     use H();

     use old(H());

-    assert H() == old(H()) + 1;

+    assert HH() == old(HH()) + 1;

+  }

+

+  method Q4(other: T)

+    requires other != null && other != this;

+    modifies other;

+  {

+    other.x := other.x + 1;

+    assert HH() == old(HH());  // frame axiom for H still works

+  }

+

+  method Q5(other: T)

+    requires other != null && other != this;

+    modifies this;

+  {

+    x := x + 1;

+    assert other.HH() == old(other.HH());  // frame axiom for H still works

+  }

+

+  method Q6(other: T)

+    requires other != null;

+    modifies this;

+  {

+    x := x + 1;

+    assert other.HH() == old(other.HH());  // error: 'other' may equal 'this', in which

+                                           // case nothing is known about how H() changed

+  }

+

+  use function K(): bool

+    reads this;

+    decreases 0;

+  {

+    x <= 100

+  }

+  use function KK(): bool

+    reads this;

+    decreases 1;

+  {

+    K()

+  }

+

+  method R0()

+    requires KK();

+    modifies this;

+  {

+    x := x - 1;

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

+  }

+

+  method R1()

+    requires KK();

+    modifies this;

+  {

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

+    x := x - 1;

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

+  }

+

+  method R2()

+    requires KK();

+    modifies this;

+  {

+    x := x - 1;

+    use K();

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

+  }

+

+  method R3()

+    requires KK();

+    modifies this;

+  {

+    use K();

+    x := x - 1;

+    use K();

+    assert KK();  // thar it is

+  }

+}

+

+class Recursive {

+  use function Gauss(n: int): int

+    requires 0 <= n;

+    decreases n;

+  {

+    if n == 0 then 0 else Gauss(n-1) + n

+  }

+

+  ghost method G(n: int)

+    requires 0 <= n;

+    ensures Gauss(n) == (n+1)*n / 2;

+  {

+    var k := 0;

+    while (k < n)

+      invariant k <= n;

+      invariant Gauss(k) == (k+1)*k / 2;

+      decreases n - k;

+    {

+      k := k + 1;

+    }

+  }

+

+  use function Fib(n: int): int

+    requires 0 <= n;

+    decreases n;

+  {

+    if n < 2 then n else Fib(n-2) + Fib(n-1)

+  }

+

+  method F0()

+  {

+    assert Fib(2) == 1;  // error (does not know about Fib for the recursive calls)

+  }

+

+  method F1()

+  {

+    assert Fib(0) == 0;

+    assert Fib(1) == 1;

+    assert Fib(2) == 1;  // now it knows

+  }

+

+  method F2()

+  {

+    assert Fib(0) == 0;

+    use Fib(1);

+    assert Fib(2) == 1;  // now it knows, too

   }

 }

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index f1bcfde0..64efe27b 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -20,7 +20,8 @@ for %%f in (BQueue.bpl) do (
 for %%f in (TypeTests.dfy SmallTests.dfy Queue.dfy ListCopy.dfy

             BinaryTree.dfy ListReverse.dfy ListContents.dfy

             SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy

-            TypeParameters.dfy Datatypes.dfy) do (

+            TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy

+            SumOfCubes.dfy) do (

   echo.

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

   %DAFNY_EXE% %* %%f