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

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);