Redesigned the encoding of Dafny generics, including the built-in types set and seq.

Regrettably, these changes--although improvements in Dafny's functionality--have caused Test/dafny0/BinaryTree.bpl and Test/dafny0/SchorrWaite.dfy to be significantly slower (the dafny0 test directory now takes 6:11 whereas it used to take 1:43).

Improved some of the VSI-Benchmarks to use generics more fully, where the previous designed had just crashed.

Included the previously commented-out loop invariants and assertions in VSI-Benchmarks/b8.dfy.

Added a space in the pretty printing of Boogie coercion expressions.

1 files changed, 5 insertions, 5 deletions

diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index f7d51058..ddad7599 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -7,22 +7,22 @@
 

 

 class Queue<T> {

-  var contents: seq<int>;

+  var contents: seq<T>;

   method Init();

     modifies this;

     ensures |contents| == 0;

-  method Enqueue(x: int);

+  method Enqueue(x: T);

     modifies this;

     ensures contents == old(contents) + [x];

-  method Dequeue() returns (x: int);

+  method Dequeue() returns (x: T);

     requires 0 < |contents|;

     modifies this;

     ensures contents == old(contents)[1..] && x == old(contents)[0];

-  function Head(): int

+  function Head(): T

     requires 0 < |contents|;

     reads this;

   { contents[0] }

-  function Get(i: int): int

+  function Get(i: int): T

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

     reads this;

   { contents[i] }