Dafny:

Previously, a "use" function was one whose definition was applied only in limited ways, namely when the function was uttered in a program (possibly in a "use" statement).  Now, recursive functions are always limited, unless declared with the new modifier "unlimited".  Non-recursive functions are always unlimited.  Also new is that only function calls within the same SCC of the call graph use the limited form of the callee.
The "use" modifier is no longer supported.  The "use" statement is still supported, now for both limited and unlimited functions; but it's probably better and easier to just explicitly mention a function in an assertion, if needed.

8 files changed, 43 insertions, 44 deletions

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 86c12854..ec255ed1 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -53,10 +53,10 @@ class Array {
       i := i + 1;

     }

   }

-  function method Length(): int

+   function method Length(): int

     reads this;

   { |contents| }

-  function method Get(i: int): int

+   function method Get(i: int): int

     requires 0 <= i && i < |contents|;

     reads this;

   { contents[i] }

@@ -88,14 +88,9 @@ method Main() {
 

 method TestSearch(a: Array, key: int)

   requires a != null;

-  requires (forall i, j ::

-              0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));

+  requires (forall i, j :: 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));

 {

-  assert (forall i, j ::

-              0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));

   var b := new Benchmark2;

-  assert (forall i, j ::

-              0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));

   call r := b.BinarySearch(a, key);

   print "Looking for key=", key, ", result=", r, "\n";

 }

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 3718618e..7ac8ff37 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -321,35 +321,35 @@ Dafny program verifier finished with 10 verified, 0 errors
 Dafny program verifier finished with 13 verified, 0 errors

 

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

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

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

 Execution trace:

     (0,0): anon0

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

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

 Execution trace:

     (0,0): anon0

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

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

 Execution trace:

     (0,0): anon0

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

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

 Execution trace:

     (0,0): anon0

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

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

 Execution trace:

     (0,0): anon0

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

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

 Execution trace:

     (0,0): anon0

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

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

 Execution trace:

     (0,0): anon0

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

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

 Execution trace:

     (0,0): anon0

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

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

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 38 verified, 9 errors

+Dafny program verifier finished with 39 verified, 9 errors

 

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

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

diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
index 714e9d58..8b4892dd 100644
--- a/Test/dafny0/BinaryTree.dfy
+++ b/Test/dafny0/BinaryTree.dfy
@@ -64,10 +64,12 @@ class IntSet {
       m := n;

     } else {

       if (x < n.data) {

+        assert n.right == null || n.right.Valid();

         call t := InsertHelper(x, n.left);

         n.left := t;

         n.footprint := n.footprint + n.left.footprint;

       } else {

+        assert n.left == null || n.left.Valid();

         call t := InsertHelper(x, n.right);

         n.right := t;

         n.footprint := n.footprint + n.right.footprint;

diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index 4bf6ae30..b69fa4f6 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -176,7 +176,7 @@ class StatementTwoShoes {
     }

   }

 

-  use function G(w: int): int { 5 }

+  function G(w: int): int { 5 }

   function method H(x: int): int;

 

   method V(s: set<StatementTwoShoes>, a: int, b: int)

diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy
index 7f0085e0..62636ce5 100644
--- a/Test/dafny0/ListContents.dfy
+++ b/Test/dafny0/ListContents.dfy
@@ -5,7 +5,7 @@ class Node<T> {
   var data: T;

   var next: Node<T>;

 

-  use function Valid(): bool

+  function Valid(): bool

     reads this, footprint;

   {

     this in this.footprint && null !in this.footprint &&

diff --git a/Test/dafny0/Substitution.dfy b/Test/dafny0/Substitution.dfy
index 195c9257..9668afb9 100644
--- a/Test/dafny0/Substitution.dfy
+++ b/Test/dafny0/Substitution.dfy
@@ -67,7 +67,7 @@ static function Substitute(e: Expression, v: int, val: int): Expression
   case Nary(op, args) => #Expression.Nary(op, SubstSeq(e, args, v, val))

 }

 

-use static function SubstSeq(/*ghost*/ parent: Expression,

+static function SubstSeq(/*ghost*/ parent: Expression,

                          q: seq<Expression>, v: int, val: int): seq<Expression>

   requires (exists op,args :: parent == #Expression.Nary(op, args) && q <= args);

   decreases parent, false, q;

diff --git a/Test/dafny0/SumOfCubes.dfy b/Test/dafny0/SumOfCubes.dfy
index 42a82fe6..f3359778 100644
--- a/Test/dafny0/SumOfCubes.dfy
+++ b/Test/dafny0/SumOfCubes.dfy
@@ -1,5 +1,5 @@
 class SumOfCubes {

-  static use function SumEmUp(n: int, m: int): int

+  static function SumEmUp(n: int, m: int): int

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

     decreases m - n;

   {

@@ -42,7 +42,7 @@ class SumOfCubes {
     call Lemma3(0, k);

   }

 

-  static use function GSum(k: int): int

+  static function GSum(k: int): int

     requires 0 <= k;

     decreases k;

   {

@@ -87,7 +87,7 @@ class SumOfCubes {
     }

   }

 

-  static use function SumEmDown(n: int, m: int): int

+  static function SumEmDown(n: int, m: int): int

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

     decreases m;

   {

diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy
index 58cb6bea..aaf41190 100644
--- a/Test/dafny0/Use.dfy
+++ b/Test/dafny0/Use.dfy
@@ -1,10 +1,12 @@
 class T {

   var x: int;

 

-  use function F(y: int): int

+  function F(y: int): int

+    decreases false;

   {

-    2*y

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

@@ -14,9 +16,9 @@ class T {
     assert F(72) == 14;  // error (just plain wrong)

   }

 

-  use function FF(y: int): int

+  function FF(y: int): int

   {

-    F(y)

+    FEntry(y)

   }

 

   method MM() {

@@ -33,11 +35,11 @@ class T {
     assert FF(9) == 18;  // error (definition of F not engaged; the use of FF does not help)

   }

 

-  use function G(y: int): bool

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

   {

-    0 <= y

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

   }

-  use function GG(y: int): bool

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

   {

     G(y)

   }

@@ -52,13 +54,13 @@ class T {
     assert !GG(-7);  // error (the negation disables the expansion of GG in the assert)

   }

 

-  use function H(): int

-    reads this;

+  function H(): int

+    reads this; decreases false;

   {

-    x

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

   }

-  use function HH(): int

-    reads this;

+  unlimited function HH(): int

+    reads this; decreases true;

   {

     H()

   }

@@ -125,13 +127,13 @@ class T {
                                            // case nothing is known about how H() changed

   }

 

-  use function K(): bool

-    reads this;

+  function K(): bool

+    reads this; decreases false;

   {

-    x <= 100

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

   }

-  use function KK(): bool

-    reads this;

+  unlimited function KK(): bool

+    reads this; decreases true;

   {

     K()

   }

@@ -148,7 +150,7 @@ class T {
     requires KK();

     modifies this;

   {

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

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

     x := x - 1;

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

   }

@@ -174,7 +176,7 @@ class T {
 }

 

 class Recursive {

-  use function Gauss(n: int): int

+  function Gauss(n: int): int

     requires 0 <= n;

     decreases n;

   {

@@ -195,7 +197,7 @@ class Recursive {
     }

   }

 

-  use function Fib(n: int): int

+  function Fib(n: int): int

     requires 0 <= n;

     decreases n;

   {