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

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;