Initial version of VSI Benchmarks 1 - 8

1 files changed, 375 insertions, 0 deletions

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
new file mode 100644
index 00000000..01b10a5a
--- /dev/null
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -0,0 +1,375 @@
+// Benchmark 8

+

+// A dictionary is a mapping between words and sequences of words

+// to set up the dictionary in main we will read a stream of words and put them into the mapping - the first element of the stream is the term, 

+// 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>;

+  method Init();

+    modifies this;

+    ensures |contents| == 0;

+  method Enqueue(x: Word);

+    modifies this;

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

+  method Dequeue() returns (x: Word);

+    requires 0 < |contents|;

+    modifies this;

+    ensures contents == old(contents)[1..] && x == old(contents)[0];

+  function Head(): Word

+    requires 0 < |contents|;

+    reads this;

+  { contents[0] }

+  function Get(i: int): Word

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

+    reads this;

+  { contents[i] }

+}

+

+

+class Glossary {

+ 

+ 

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

+    requires q != null;

+    modifies q;

+    ensures r != null && fresh(r);

+    ensures |r.contents| == |old(q.contents)|;

+    ensures (forall i, j :: 0 <= i && i < j && j < |r.contents| ==>

+                r.Get(i).AtMost(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]]);

+  

+

+

+	method main()

+	{

+		var rs:= new ReaderStream;

+		call rs.Open();

+		var glossary := new Map<Word,seq<Word>>;

+		call glossary.Init();

+		var q:= new Queue<Word>;

+		call q.Init();

+		

+		while (true)

+			invariant rs.Valid() && fresh(rs.footprint);

+			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 !(q in rs.footprint);

+			//  ** invariant q.contents == glossary.keys; need a quantifer to express this (map doesnt necessarily add to end)

+			// we leave out the decreases clause - unbounded stream

+		{

+			var term,definition;

+			call term,definition := readDefinition(rs);

+			if (term == null)

+			{

+				break;

+			}	

+			call glossary.Add(term,definition);	

+			call q.Enqueue(term);

+		}	

+		

+		call rs.Close();

+		var p;

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

+	    var wr := new WriterStream;

+	    call wr.Create();

+	    

+	    while (0<|q.contents|)

+			invariant wr.Valid() && fresh(wr.footprint);

+			invariant glossary.Valid();

+			invariant !(glossary in wr.footprint);

+			invariant !(null in glossary.keys);

+			invariant !(q in wr.footprint);

+			decreases |q.contents|;

+		{

+			var term, present, definition;

+			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

+			

+			// write term with a html anchor

+			call wr.PutWordInsideTag(term, term);

+			var i := 0;

+			

+			while ( i < |definition|)

+		    invariant wr.Valid() && fresh(wr.footprint);

+			invariant !(glossary in wr.footprint);

+			invariant !(q in wr.footprint); 

+				decreases |definition| -i;

+			{

+				var w := definition[i];

+				var d;

+				assume w != null; // to convert this into an assert we need invariant *** above

+				call present, d := glossary.Find(w);

+				if (present)

+				{

+					call wr. PutWordInsideHyperlink(w, w);

+				}

+				else 

+				{

+					call wr. PutWord(w);

+				}

+				i:= i +1;

+			}

+		}

+		call wr.Close();		  

+	}

+	

+

+	method readDefinition(rs:ReaderStream) returns (term:Word, definition:seq<Word>)

+	requires rs != null && rs.Valid();

+	modifies rs.footprint;

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

+	ensures term != null ==> !(null in definition);

+	{

+		call term := rs.GetWord();

+		if (term != null)

+		{

+			definition := [];

+			while (true)

+				invariant rs.Valid() && fresh(rs.footprint - old(rs.footprint));

+				invariant !(null in definition);

+			{

+				var w;

+				call w := rs.GetWord();

+				if (w == null)

+				{

+					break;

+				}

+				definition := definition + [w];

+			}

+		}

+		

+	}

+  

+  }

+  

+  class Word

+  {

+  

+	function AtMost(w:Word) :bool;

+  

+  }

+  

+  class ReaderStream {

+  var footprint:set<object>;

+  var isOpen:bool;

+  

+  function Valid():bool

+  reads this, footprint;

+  {

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

+  }

+  

+  method Open() //reading

+  modifies this;

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

+  {

+		footprint := {this}; 

+		isOpen :=true;

+  }

+  

+  method GetWord()returns(x:Word)

+  requires Valid() ;

+  modifies footprint;

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

+  {

+	

+  }

+  

+ method Close() 

+ requires Valid();

+ modifies footprint;

+ {

+	isOpen := false;

+	

+ }

+  

+}

+

+class WriterStream {

+  var footprint:set<object>;

+  var stream:seq<int>; 

+  var isOpen:bool;

+  

+  function Valid():bool

+  reads this, footprint;

+  {

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

+  }

+  

+method Create() //writing

+  modifies this;

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

+  ensures stream == [];

+  {

+		stream := [];

+		footprint := {this}; 

+		isOpen:= true;

+  }

+  method GetCount() returns (c:int)

+  requires Valid();

+  ensures 0<=c;

+  {

+		c:=|stream|;

+  }

+  

+  method PutWord(w:Word )

+  requires Valid();

+  requires  w != null; 

+  modifies footprint;

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

+  ensures old(stream)<= stream;

+  {

+  }

+  method PutWordInsideTag(tag:Word,w:Word )

+  requires Valid();

+  requires tag != null && w != null;

+  modifies footprint;

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

+  ensures old(stream)<= stream;

+  {

+  }

+  

+  method PutWordInsideHyperlink(tag:Word,w:Word )

+  requires Valid();

+  requires tag != null && w != null;

+  modifies footprint;

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

+  ensures old(stream)<= stream;

+  {

+  }

+   

+ method Close() 

+ requires Valid();

+ modifies footprint;

+ {

+	isOpen := false;

+	

+ }

+  

+}

+

+  

+  

+  

+class Map<Key,Value> {

+  var keys: seq<Key>;

+  var values: seq<Value>;

+  

+

+  function Valid(): bool

+    reads this;

+  {

+    |keys| == |values| &&

+    (forall i, j :: 0 <= i && i < j && j < |keys| ==> keys[i] != keys[j])

+  }

+

+  method Init()

+    modifies this;

+    ensures Valid() && |keys| == 0;

+  {

+    keys := [];

+    values := [];

+  }

+

+  method Find(key: Key) returns (present: bool, val: Value)

+    requires Valid();

+    ensures !present ==> !(key in keys);

+    ensures present ==> (exists i :: 0 <= i && i < |keys| &&

+                                     keys[i] == key && values[i] == val);

+  {

+    var j;

+    call j := FindIndex(key);

+    if (j == -1) {

+      present := false;

+    } else {

+      present := true;

+      val := values[j];

+    }

+  }

+

+  method Add(key: Key, val: 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]);

+  {

+    var j;

+    call j := FindIndex(key);

+    if (j == -1) {

+      keys := keys + [key];

+      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

+    }

+  }

+

+  method Remove(key: Key)

+    requires Valid();

+    modifies this;

+    ensures Valid();

+    // no key is introduced:

+    ensures (forall k :: k in keys ==> k in old(keys));

+    // at most one key is removed:

+    ensures (forall k :: k in old(keys) ==> k in keys || k == key);

+    // the given key is not there:

+    // other values don't change:

+    ensures !(key in old(keys)) ==> keys == old(keys) && values == old(values);

+    ensures key in old(keys) ==>

+            !(key in keys) &&

+            (exists h ::

+              0 <= h && h <= |keys| &&

+              keys[..h] == old(keys)[..h] &&

+              values[..h] == old(values)[..h] &&

+              keys[h..] == old(keys)[h+1..] &&

+              values[h..] == old(values)[h+1..]);

+  {

+    var j;

+    call j := FindIndex(key);

+    if (0 <= j) {

+      keys := keys[..j] + keys[j+1..];

+      values := values[..j] + values[j+1..];

+    }

+  }

+

+  method FindIndex(key: Key) returns (idx: int)

+    requires Valid();

+    ensures -1 <= idx && idx < |keys|;

+    ensures idx == -1 ==> !(key in keys);

+    ensures 0 <= idx ==> keys[idx] == key;

+  {

+    var j := 0;

+    while (j < |keys|)

+      invariant j <= |keys|;

+      invariant !(key in keys[..j]);

+      decreases |keys| -j;

+    {

+      if (keys[j] == key) {

+        idx := j;

+        return;

+      }

+      j := j + 1;

+    }

+    idx := -1;

+  }

+}