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.

8 files changed, 104 insertions, 62 deletions

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 4f717f48..4f44612d 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -13,22 +13,22 @@
 //would be nice if we could mark pperm as a ghost variable

 

 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] }

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

     }

diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index 48306e9b..d320f9e9 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -1,7 +1,7 @@
 

-class Collection {

+class Collection<T> {

   var footprint:set<object>;

-  var elements:seq<int>;

+  var elements:seq<T>;

   

   function Valid():bool

   reads this, footprint;

@@ -24,7 +24,7 @@ class Collection {
 		footprint := {this}; 

   }

   

-  method GetItem(i:int ) returns (x:int)

+  method GetItem(i:int ) returns (x:T)

   requires Valid();

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

   ensures elements[i] ==x;

@@ -32,7 +32,7 @@ class Collection {
 		x:=elements[i];

   }

   

-  method Add(x:int )

+  method Add(x:T )

   requires Valid();

   modifies footprint;

   ensures Valid() && fresh(footprint - old(footprint));

@@ -41,21 +41,21 @@ class Collection {
 		elements:= elements + [x];

   }

   

-  method GetIterator() returns (iter:Iterator)

+  method GetIterator() returns (iter:Iterator<T>)

   requires Valid();

   ensures iter != null && iter.Valid();

   ensures fresh(iter.footprint) && iter.pos == -1;

   ensures iter.c == this;

   {

-      iter:= new Iterator;

+      iter:= new Iterator<T>;

       call iter.Init(this);

   }

   

 }

 

-class Iterator {

+class Iterator<T> {

  

-  var c:Collection;

+  var c:Collection<T>;

   var pos:int;

   

   var footprint:set<object>;

@@ -66,7 +66,7 @@ class Iterator {
 		this in footprint && c!= null && -1<= pos && null !in footprint

   }

   

-  method Init(coll:Collection)

+  method Init(coll:Collection<T>)

   requires coll != null;

   modifies this;

   ensures Valid() && fresh(footprint -{this}) && pos ==-1;

@@ -94,7 +94,7 @@ class Iterator {
 	0<= pos && pos < |c.elements|

  }

  

- method GetCurrent() returns (x:int)

+ method GetCurrent() returns (x:T)

  requires Valid() && HasCurrent();

  ensures c.elements[pos] == x;

   {

@@ -108,7 +108,7 @@ class Client
 

 	method Main()

 	{

-		var c:= new Collection;

+		var c:= new Collection<int>;

 		call c.Init();

 		call c.Add(33);

 		call c.Add(45);

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] }

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

     }

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 64c43c87..78982f01 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -96,5 +96,11 @@ Execution trace:
 Dafny program verifier finished with 5 verified, 3 errors

 

 -------------------- TypeParameters.dfy --------------------

+TypeParameters.dfy(41,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    (0,0): anon0

+TypeParameters.dfy(63,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 3 verified, 0 errors

+Dafny program verifier finished with 7 verified, 2 errors

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;

+  }

+}

diff --git a/Test/inline/Answer b/Test/inline/Answer
index 43ec6740..8f2c34e4 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -961,12 +961,12 @@ function {:inline true} foo(x: int) returns (bool)
 function {:inline false} foo2(x: int) returns (bool);

 

 // autogenerated definition axiom

-axiom (forall x: int :: {:inline false} { foo2(x):bool } foo2(x):bool == (x > 0));

+axiom (forall x: int :: {:inline false} { foo2(x): bool } foo2(x): bool == (x > 0));

 

 function foo3(x: int) returns (bool);

 

 // autogenerated definition axiom

-axiom (forall x: int :: { foo3(x):bool } foo3(x):bool == (x > 0));

+axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0));

 

 Boogie program verifier finished with 0 verified, 0 errors

 fundef2.bpl(6,3): Error BP5001: This assertion might not hold.