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.

1 files changed, 3 insertions, 8 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";

 }