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

1 files changed, 172 insertions, 11 deletions

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

   }

 }