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, 44 insertions, 0 deletions

diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index 3f57f369..794f2f95 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -19,3 +19,47 @@ class C<U> {
 

   function G<Y>(): Y;

 }

+

+class SetTest {

+  method Add<T>(s: set<T>, x: T) returns (t: set<T>)

+    ensures t == s + {x};

+  {

+    t := s + {x};

+  }

+

+  method Good()

+  {

+    var s := {2, 5, 3};

+    call t := Add(s, 7);

+    assert {5,7,2,3} == t;

+  }

+

+  method Bad()

+  {

+    var s := {2, 50, 3};

+    call t := Add(s, 7);

+    assert {5,7,2,3} == t;  // error

+  }

+}

+

+class SequenceTest {

+  method Add<T>(s: seq<T>, x: T) returns (t: seq<T>)

+    ensures t == s + [x];

+  {

+    t := s + [x];

+  }

+

+  method Good()

+  {

+    var s := [2, 5, 3];

+    call t := Add(s, 7);

+    assert [2,5,3,7] == t;

+  }

+

+  method Bad()

+  {

+    var s := [2, 5, 3];

+    call t := Add(s, 7);

+    assert [2,5,7,3] == t || [2,5,3] == t;

+  }

+}