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, 4 insertions, 11 deletions

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index 5a9d46c8..e3a99884 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -43,16 +43,10 @@ class Map<Key,Value> {
     requires Valid();

     modifies this;

     ensures Valid();

-    // no key is lost:

-    ensures (forall k :: k in old(keys) ==> k in keys);

-    // at most one key is introduced:

-    ensures (forall k :: k in keys ==> k in old(keys) || k == key);

-    // the given key has the given value:

-    ensures (exists i :: 0 <= i && i < |keys| &&

-                         keys[i] == key && values[i] == val);

-    // other values don't change:

-    ensures (forall i :: 0 <= i && i < |keys| && keys[i] != key ==>

-                values[i] == old(values)[i]);

+    ensures (forall i :: 0 <= i && i < |keys| && old(keys)[i] == key ==>

+              keys[i] == key && values[i] == val &&

+              (forall j :: 0 <= j && j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j]));

+    ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val];

   {

     call j := FindIndex(key);

     if (j == -1) {

@@ -60,7 +54,6 @@ class Map<Key,Value> {
       values := values + [val];

       assert values[|keys|-1] == val;  // lemma

     } else {

-      keys := keys[..j] + [key] + keys[j+1..];

       values := values[..j] + [val] + values[j+1..];

       assert values[j] == val; //lemma

     }