Dafny:

* First crack at a compiler (/compile:1 writes out.cs, if Dafny program verifies)
* Added "print" statement (to make running compiled programs more interesting)
* Changed name of default class from $default to _default
Boogie:
* Included "lambda" as a keyword in emacs and latex style files

1 files changed, 47 insertions, 49 deletions

diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index 90f484bd..9b244e69 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -1,51 +1,51 @@
 

 class Collection<T> {

-  var footprint:set<object>;

+  ghost var footprint:set<object>;

   var elements:seq<T>;

   

   function Valid():bool

-  reads this, footprint;

+    reads this, footprint;

   {

     this in footprint

   }

   

   method GetCount() returns (c:int)

-  requires Valid();

-  ensures 0<=c;

+    requires Valid();

+    ensures 0<=c;

   {

     c:=|elements|;

   }

   

   method Init()

-  modifies this;

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

+    modifies this;

+    ensures Valid() && fresh(footprint -{this});

   {

     elements := [];

     footprint := {this}; 

   }

   

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

-  requires Valid();

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

-  ensures elements[i] ==x;

+    requires Valid();

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

+    ensures elements[i] ==x;

   {

     x:=elements[i];

   }

   

   method Add(x:T )

-  requires Valid();

-  modifies footprint;

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

-  ensures elements == old(elements) + [x];

+    requires Valid();

+    modifies footprint;

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

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

   {

     elements:= elements + [x];

   }

   

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

-  requires Valid();

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

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

-  ensures iter.c == this;

+    requires Valid();

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

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

+    ensures iter.c == this;

   {

       iter:= new Iterator<T>;

       call iter.Init(this);

@@ -58,49 +58,48 @@ class Iterator<T> {
   var c:Collection<T>;

   var pos:int;

   

-  var footprint:set<object>;

+  ghost var footprint:set<object>;

   

   function Valid():bool

-  reads this, footprint;

+    reads this, footprint;

   {

-    this in footprint && c!= null && -1<= pos && null !in footprint

+    this in footprint && c != null && -1 <= pos && null !in footprint

   }

   

   method Init(coll:Collection<T>)

-  requires coll != null;

-  modifies this;

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

-  ensures c == coll;

+    requires coll != null;

+    modifies this;

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

+    ensures c == coll;

   {

-    c:= coll;

-    pos:=-1;

+    c := coll;

+    pos := -1;

     footprint := {this}; 

   }

   

   method MoveNext() returns (b:bool)

-  requires Valid();

-  modifies footprint;

-  ensures fresh(footprint - old(footprint)) &&  Valid()  && pos == old(pos) + 1;

-  ensures b == HasCurrent() && c == old(c);

+    requires Valid();

+    modifies footprint;

+    ensures fresh(footprint - old(footprint)) &&  Valid()  && pos == old(pos) + 1;

+    ensures b == HasCurrent() && c == old(c);

   {

-  pos:= pos+1;

-  b:= pos < |c.elements|;

+    pos := pos+1;

+    b := pos < |c.elements|;

   }

   

- function HasCurrent():bool //???

-   requires Valid();

-   reads this, c;

- {

-  0<= pos && pos < |c.elements|

- }

- 

- method GetCurrent() returns (x:T)

- requires Valid() && HasCurrent();

- ensures c.elements[pos] == x;

+  function HasCurrent():bool //???

+    requires Valid();

+    reads this, c;

   {

-    x:=c.elements[pos];

+    0 <= pos && pos < |c.elements|

   }

  

+  method GetCurrent() returns (x:T)

+    requires Valid() && HasCurrent();

+    ensures c.elements[pos] == x;

+  {

+    x := c.elements[pos];

+  }

 } 

 

 class Client

@@ -108,13 +107,13 @@ class Client
 

   method Main()

   {

-    var c:= new Collection<int>;

+    var c := new Collection<int>;

     call c.Init();

     call c.Add(33);

     call c.Add(45);

     call c.Add(78);

     

-    var s:= [ ];

+    var s := [];

     

     call iter := c.GetIterator();

     call b := iter.MoveNext();

@@ -126,9 +125,9 @@ class Client
       invariant iter.c == c;

       decreases |c.elements| - iter.pos;

     {   

-      call x:= iter.GetCurrent();

-      s:= s + [x];

-      call b:= iter.MoveNext();

+      call x := iter.GetCurrent();

+      s := s + [x];

+      call b := iter.MoveNext();

     }

     

     assert s == c.elements; //verifies that the iterator returns the correct things

@@ -136,4 +135,3 @@ class Client
   }

   

 }

-