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

8 files changed, 209 insertions, 152 deletions

diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer
index a0ae9d01..926a4da3 100644
--- a/Test/VSI-Benchmarks/Answer
+++ b/Test/VSI-Benchmarks/Answer
@@ -1,11 +1,11 @@
 

 -------------------- b1.dfy --------------------

 

-Dafny program verifier finished with 4 verified, 0 errors

+Dafny program verifier finished with 10 verified, 0 errors

 

 -------------------- b2.dfy --------------------

 

-Dafny program verifier finished with 6 verified, 0 errors

+Dafny program verifier finished with 8 verified, 0 errors

 

 -------------------- b3.dfy --------------------

 

diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy
index 70522aaf..1ab76a78 100644
--- a/Test/VSI-Benchmarks/b1.dfy
+++ b/Test/VSI-Benchmarks/b1.dfy
@@ -47,4 +47,29 @@ class Benchmark1 {
       call r := Add(r, y);

     }

   }

+

+  method Main() {

+    call TestAdd(3, 180);

+    call TestAdd(3, -180);

+    call TestAdd(0, 1);

+

+    call TestMul(3, 180);

+    call TestMul(3, -180);

+    call TestMul(180, 3);

+    call TestMul(-180, 3);

+    call TestMul(0, 1);

+    call TestMul(1, 0);

+  }

+

+  method TestAdd(x: int, y: int) {

+    print x, " + ", y, " = ";

+    call z := Add(x, y);

+    print z, "\n";

+  }

+

+  method TestMul(x: int, y: int) {

+    print x, " * ", y, " = ";

+    call z := Mul(x, y);

+    print z, "\n";

+  }

 }

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 7d964061..0cae993a 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -1,6 +1,4 @@
 

-// Note:  There is a bug in the well-formedness of functions.  In particular,

-// it doesn't look at the requires clause (in the proper way).  Fixed!

 // Note:Implemented arrays as Dafny does not provide them

 

 class Benchmark2 {

@@ -40,10 +38,21 @@ class Benchmark2 {
 

 class Array {

   var contents: seq<int>;

-  method Init(n: int);

+  method Init(n: int)

     requires 0 <= n;

     modifies this;

     ensures |contents| == n;

+  {

+    var i := 0;

+    contents := [];

+    while (i < n)

+      invariant i <= n && i == |contents|;

+      decreases n - i;

+    {

+      contents := contents + [0];

+      i := i + 1;

+    }

+  }

   function method Length(): int

     reads this;

   { |contents| }

@@ -51,11 +60,47 @@ class Array {
     requires 0 <= i && i < |contents|;

     reads this;

   { contents[i] }

-  method Set(i: int, x: int);

+  method Set(i: int, x: int)

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

     modifies this;

     ensures |contents| == |old(contents)|;

     ensures contents[..i] == old(contents[..i]);

     ensures contents[i] == x;

     ensures contents[i+1..] == old(contents[i+1..]);

+  {

+    contents := contents[i := x];

+  }

+}

+

+/******

+method Main() {

+  var a := new Array;

+  call a.Init(5);

+  call a.Set(0, -4);

+  call a.Set(1, -2);

+  call a.Set(2, -2);

+  call a.Set(3, 0);

+  call a.Set(4, 25);

+  call TestSearch(a, 4);

+  call TestSearch(a, -8);

+  call TestSearch(a, -2);

+  call TestSearch(a, 0);

+  call TestSearch(a, 23);

+  call TestSearch(a, 25);

+  call TestSearch(a, 27);

+}

+

+method TestSearch(a: Array, key: int)

+  requires a != null;

+  requires (forall i, j ::

+              0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));

+{

+  assert (forall i, j ::

+              0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));

+  var b := new Benchmark2;

+  assert (forall i, j ::

+              0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));

+  call r := b.BinarySearch(a, key);

+  print "Looking for key=", key, ", result=", r, "\n";

 }

+******/

diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy
index 2e274845..94fe1eaa 100644
--- a/Test/VSI-Benchmarks/b5.dfy
+++ b/Test/VSI-Benchmarks/b5.dfy
@@ -4,9 +4,9 @@ class Queue<T> {
   var head: Node<T>;

   var tail: Node<T>;

 

-  var contents: seq<T>;

-  var footprint: set<object>;

-  var spine: set<Node<T>>;

+  ghost var contents: seq<T>;

+  ghost var footprint: set<object>;

+  ghost var spine: set<Node<T>>;

 

   function Valid(): bool

     reads this, footprint;

@@ -124,8 +124,8 @@ class Node<T> {
   var data: T;

   var next: Node<T>;

 

-  var tailContents: seq<T>;

-  var footprint: set<object>;

+  ghost var tailContents: seq<T>;

+  ghost var footprint: set<object>;

 

   function Valid(): bool

     reads this, footprint;

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
   }

   

 }

-

diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index ddad7599..e5af6357 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -29,84 +29,78 @@ class Queue<T> {
 }

 

 class Stream {

-  var footprint:set<object>;

+  ghost var footprint:set<object>;

   var stream:seq<int>; 

   var isOpen:bool;

   

   function Valid():bool

-  reads this, footprint;

+    reads this, footprint;

   {

-	null !in footprint && this in footprint && isOpen

+    null !in footprint && this in footprint && isOpen

   }

   

   method GetCount() returns (c:int)

-  requires Valid();

-  ensures 0<=c;

+    requires Valid();

+    ensures 0 <= c;

   {

-		c:=|stream|;

+    c := |stream|;

   }

   

   method Create() //writing

-  modifies this;

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

-  ensures stream == [];

+    modifies this;

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

+    ensures stream == [];

   {

-		stream := [];

-		footprint := {this}; 

-		isOpen:= true;

+    stream := [];

+    footprint := {this}; 

+    isOpen := true;

   }

  

   method Open() //reading

-  modifies this;

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

+    modifies this;

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

   {

-		footprint := {this}; 

-		isOpen :=true;

+    footprint := {this}; 

+    isOpen := true;

   }

   

   method PutChar(x:int )

-  requires Valid();

-  modifies footprint;

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

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

+    requires Valid();

+    modifies footprint;

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

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

   {

-		stream:= stream + [x];

+    stream:= stream + [x];

   }

   

   method GetChar()returns(x:int)

-  requires Valid() && 0< |stream|;

-  modifies footprint;

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

-  ensures x ==old(stream)[0];

-  ensures stream == old(stream)[1..]; 

+    requires Valid() && 0 < |stream|;

+    modifies footprint;

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

+    ensures x ==old(stream)[0];

+    ensures stream == old(stream)[1..]; 

   {

-		x := stream[0];

-		stream:= stream[1..];

-	

+    x := stream[0];

+    stream := stream[1..];

   }

  

- method AtEndOfStream() returns(eos:bool)

- requires Valid();

- ensures eos   <==> |stream| ==0; 

- {

-	eos:= |stream| ==0; 

- }

-  

- method Close() 

- requires Valid();

- modifies footprint;

- {

-	isOpen := false;

-	

- }

+  method AtEndOfStream() returns(eos:bool)

+    requires Valid();

+    ensures eos  <==> |stream| == 0;

+  {

+    eos := |stream| == 0; 

+  }

   

+  method Close() 

+    requires Valid();

+    modifies footprint;

+  {

+    isOpen := false;

+  }

 }

 

 

-

 class Client {

-

-

   method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>);

     requires q != null;

     modifies q;

@@ -115,49 +109,44 @@ class Client {
     ensures (forall i, j :: 0 <= i && i < j && j < |r.contents| ==>

                 r.Get(i) <= r.Get(j));

     //perm is a permutation

-   ensures |perm| == |r.contents|; // ==|pperm|

-   ensures (forall i: int :: 0 <= i && i < |perm|==> 0 <= perm[i] && perm[i] < |perm| );

-   ensures (forall i, j: int :: 0 <= i && i < j && j < |perm| ==> perm[i] != perm[j]); 

-   // the final Queue is a permutation of the input Queue

-  ensures (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);

+    ensures |perm| == |r.contents|; // ==|pperm|

+    ensures (forall i: int :: 0 <= i && i < |perm|==> 0 <= perm[i] && perm[i] < |perm| );

+    ensures (forall i, j: int :: 0 <= i && i < j && j < |perm| ==> perm[i] != perm[j]); 

+    // the final Queue is a permutation of the input Queue

+    ensures (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);

   

   

-	

-	method Main()

-	{

-		var rd:= new Stream;

-		call rd.Open();

-		

-		var q:= new Queue<int>;	

-		while (true)

-		 invariant rd.Valid() && fresh(rd.footprint) && fresh(q);

-		 decreases |rd.stream|;

-		{

-				call eos := rd.AtEndOfStream();

-				if (eos) 

-				{

-					break;

-				}

-				

-				call ch := rd.GetChar();	

-				call q.Enqueue(ch);	

-	    }

-	    

-	    call rd.Close();

-	    call q,perm := Sort(q);

-	    

-	    var wr:= new Stream;

-	    call wr.Create();

-	    while (0<|q.contents|)

-	    invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;

-	    decreases |q.contents|;

-		{

-				call ch:= q.Dequeue();	

-				call wr.PutChar(ch);		

-	    }

-	    call wr.Close();

-	    

-	}

-	

+  method Main()

+  {

+    var rd := new Stream;

+    call rd.Open();

+    

+    var q := new Queue<int>;  

+    while (true)

+      invariant rd.Valid() && fresh(rd.footprint) && fresh(q);

+      decreases |rd.stream|;

+    {

+      call eos := rd.AtEndOfStream();

+      if (eos) {

+        break;

+      }

+        

+      call ch := rd.GetChar();  

+      call q.Enqueue(ch);  

+    }

+      

+    call rd.Close();

+    call q,perm := Sort(q);

+      

+    var wr:= new Stream;

+    call wr.Create();

+    while (0 < |q.contents|)

+      invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;

+      decreases |q.contents|;

+    {

+      call ch := q.Dequeue();  

+      call wr.PutChar(ch);    

+    }

+    call wr.Close();

+  }

 }

-

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index fec36c29..d8ee2013 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -155,7 +155,7 @@ class Word
 }

   

 class ReaderStream {

-  var footprint:set<object>;

+  ghost var footprint:set<object>;

   var isOpen:bool;

   

   function Valid():bool

@@ -188,7 +188,7 @@ class ReaderStream {
 }

 

 class WriterStream {

-  var footprint:set<object>;

+  ghost var footprint:set<object>;

   var stream:seq<int>; 

   var isOpen:bool;

   

diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
index fa737dca..0cd898c4 100644
--- a/Test/VSI-Benchmarks/runtest.bat
+++ b/Test/VSI-Benchmarks/runtest.bat
@@ -11,5 +11,5 @@ for %%f in ( b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy
              b8.dfy ) do (

   echo.

   echo -------------------- %%f --------------------

-  %DAFNY_EXE% %* %%f

+  %DAFNY_EXE% /compile:0 %* %%f

 )