Dafny: retired "use" statements

4 files changed, 3 insertions, 267 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index c349188c..bf3ba197 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -811,43 +811,6 @@ Execution trace:
 

 Dafny program verifier finished with 44 verified, 6 errors

 

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

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

-Execution trace:

-    (0,0): anon0

-Use.dfy(26,18): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-Use.dfy(35,18): Error: assertion violation

-Execution trace:

-    (0,0): anon0

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

-Execution trace:

-    (0,0): anon0

-Use.dfy(84,17): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-Use.dfy(126,23): Error: assertion violation

-Execution trace:

-    (0,0): anon0

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

-Use.dfy(143,5): Related location: Related location

-Execution trace:

-    (0,0): anon0

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

-Use.dfy(143,5): Related location: Related location

-Execution trace:

-    (0,0): anon0

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

-Use.dfy(143,5): Related location: Related location

-Execution trace:

-    (0,0): anon0

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

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 39 verified, 10 errors

-

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

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

 Execution trace:

diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index 255b38e3..92ac0793 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -180,12 +180,12 @@ class StatementTwoShoes {
   method V(s: set<StatementTwoShoes>, a: int, b: int)

     modifies s;

   {

-    use G(12 / b);  // fine, because there are no welldefinedness checks on use statements

+

     foreach (m in s | m.x < 200)  // s may contain null, but the foreach excludes null

     {

       assume 0 <= m.x;

       assert m.x < 1000;

-      use G(5 / m.x);  // fine, because there are no welldefinedness checks on use statements

+

       m.x := m.x + 1;

     }

     foreach (m in s + {F(a)})  // error: collection expression may not be well defined (fn precondition)

diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy
deleted file mode 100644
index 502c4222..00000000
--- a/Test/dafny0/Use.dfy
+++ /dev/null
@@ -1,227 +0,0 @@
-class T {

-  var x: int;

-

-  function F(y: int): int

-    decreases false;

-  {

-    2*y + (if 1 < 0 then FEntry(y) else 0)

-  }

-  function FEntry(y: int): int decreases true; { F(y) }

-

-  method M(s: set<T>) {

-    use F(4);

-    use F(5);

-    assert F(5) == 10;

-    assert F(7) == 14;

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

-  }

-

-  function FF(y: int): int

-  {

-    FEntry(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)

-  }

-

-  function G(y: int): bool decreases false;

-  {

-    0 <= y || (1 < 0 && GG(y))

-  }

-  unlimited function GG(y: int): bool decreases true;

-  {

-    G(y)

-  }

-

-  method N(s: set<T>) {

-    use G(4);

-    use G(5);

-    use G(-5);

-    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)

-  }

-

-  function H(): int

-    reads this; decreases false;

-  {

-    x + (if 1 < 0 then HH() else 0)

-  }

-  unlimited function HH(): int

-    reads this; decreases true;

-  {

-    H()

-  }

-

-  method Q0()

-    modifies this;

-  {

-    var t := x;

-    use H();

-    assert HH() == t;

-

-    x := x + 1;

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

-  }

-

-  method Q1()

-    modifies this;

-  {

-    x := x + 1;

-    use H();

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

-  }

-

-  method Q2()

-    modifies this;

-  {

-    use H();

-    x := x + 1;

-    use H();

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

-  }

-

-  method Q3()

-    modifies this;

-  {

-    x := x + 1;

-    use H();

-    use old(H());

-    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

-  }

-

-  function K(): bool

-    reads this; decreases 0;

-  {

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

-  }

-  function KK(): bool

-    reads this; decreases 1;

-  {

-    K()

-  }

-  unlimited function KKK(): bool

-    reads this; decreases 2;

-  {

-    KK()

-  }

-

-  method R0()

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

-    modifies this;

-  {

-    x := x - 1;

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

-  }

-

-  method R1()

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

-    modifies this;

-  {

-    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 KKK();  // error: the assert expands KKK to KK, definition of KK expands K#limited (but not to K)

-  }

-

-  method R2()

-    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();  // 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 KKK();  // this expands to both KKK() and KK(); the def. of KK() expands to K#limited (but not K)

-    modifies this;

-  {

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

-    x := x - 1;

-    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

-  }

-}

-

-class Recursive {

-  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;

-    {

-      k := k + 1;

-    }

-  }

-

-  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(3) == 2;  // error (does not know about Fib for the recursive calls)

-  }

-

-  method F1()

-  {

-    assert Fib(0) == 0;

-    assert Fib(3) == 2;  // now it knows

-  }

-

-  method F2()

-  {

-    use Fib(0);

-    assert Fib(3) == 2;  // now it knows, too

-  }

-}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 0a35c871..aed9ee8a 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -16,7 +16,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

             Comprehensions.dfy Basics.dfy ControlStructures.dfy

-            Termination.dfy Use.dfy DTypes.dfy

+            Termination.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

             Refinement.dfy RefinementErrors.dfy) do (

   echo.