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, 26 insertions, 27 deletions

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 51172419..c3374605 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -5,22 +5,22 @@
 // the following words (until we read null) form the terms definition. Then the stream provides the next term etc.

 

 class Queue<T> {

-  var contents: seq<Word>;

+  var contents: seq<T>;

   method Init();

     modifies this;

     ensures |contents| == 0;

-  method Enqueue(x: Word);

+  method Enqueue(x: T);

     modifies this;

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

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

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

     requires 0 < |contents|;

     modifies this;

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

-  function Head(): Word

+  function Head(): T

     requires 0 < |contents|;

     reads this;

   { contents[0] }

-  function Get(i: int): Word

+  function Get(i: int): T

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

     reads this;

   { contents[i] }

@@ -56,18 +56,20 @@ class Glossary {
       invariant glossary.Valid();

       invariant glossary !in rs.footprint;

       invariant null !in glossary.keys;

-      //to do add invariant  invariant (forall d:: d in glossary.values ==>!(null in d)); ***

+      invariant (forall d :: d in glossary.values ==> null !in d);

       invariant q !in rs.footprint;

-      //  ** invariant q.contents == glossary.keys; need a quantifer to express this (map doesnt necessarily add to end)

+      invariant q.contents == glossary.keys;

       // we leave out the decreases clause - unbounded stream

     {

       call term,definition := readDefinition(rs);

-      if (term == null)

-      {

+      if (term == null) {

         break;

-      }    

-      call glossary.Add(term,definition);    

-      call q.Enqueue(term);

+      }

+      call present, d := glossary.Find(term);

+      if (!present) {

+        call glossary.Add(term,definition);

+        call q.Enqueue(term);

+      }

     }    

     

     call rs.Close();

@@ -79,12 +81,14 @@ class Glossary {
       invariant wr.Valid() && fresh(wr.footprint);

       invariant glossary.Valid();

       invariant glossary !in wr.footprint && null !in glossary.keys;

+      invariant (forall d :: d in glossary.values ==> null !in d);

       invariant q !in wr.footprint;

+      invariant (forall k :: k in q.contents ==> k in glossary.keys);

       decreases |q.contents|;

     {

-      call term:= q.Dequeue();

-      call present,definition:= glossary.Find(term);

-      assume present; // to change this into an assert we need the loop invariant ** above that we commented out

+      call term := q.Dequeue();

+      call present,definition := glossary.Find(term);

+      assert present;

       

       // write term with a html anchor

       call wr.PutWordInsideTag(term, term);

@@ -95,12 +99,13 @@ class Glossary {
         invariant wr.Valid() && fresh(wr.footprint);

         invariant glossary.Valid();

         invariant glossary !in wr.footprint && null !in glossary.keys;

+        invariant (forall d :: d in glossary.values ==> null !in d);

         invariant q !in wr.footprint;

         invariant qcon == q.contents;

+        invariant (forall k :: k in q.contents ==> k in glossary.keys);

         decreases |definition| -i;

       {

         var w := definition[i];

-        assume w != null; // to convert this into an assert we need invariant *** above

         call present, d := glossary.Find(w);

         if (present)

         {

@@ -130,6 +135,7 @@ class Glossary {
       while (true)

         invariant rs.Valid() && fresh(rs.footprint - old(rs.footprint));

         invariant null !in definition;

+        // we leave out the decreases clause - unbounded stream

       {

         call w := rs.GetWord();

         if (w == null)

@@ -283,16 +289,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) {

@@ -300,7 +300,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

     }