From a93807200244868daaa6e33f2f4da445fe7d52a7 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sat, 13 Feb 2010 01:17:36 +0000
Subject: 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

---
 Test/dafny0/Use.dfy | 183 ++++++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 172 insertions(+), 11 deletions(-)

(limited to 'Test/dafny0/Use.dfy')

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
   }
 }
-- 
cgit v1.2.3