From 9973fcca56f1c6345ac2697210f2f3c7662f5c30 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Thu, 6 May 2010 20:28:29 +0000 Subject: 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 --- Test/VSI-Benchmarks/Answer | 4 +- Test/VSI-Benchmarks/b1.dfy | 25 ++++++ Test/VSI-Benchmarks/b2.dfy | 53 ++++++++++++- Test/VSI-Benchmarks/b5.dfy | 10 +-- Test/VSI-Benchmarks/b6.dfy | 96 +++++++++++------------ Test/VSI-Benchmarks/b7.dfy | 167 +++++++++++++++++++--------------------- Test/VSI-Benchmarks/b8.dfy | 4 +- Test/VSI-Benchmarks/runtest.bat | 2 +- 8 files changed, 209 insertions(+), 152 deletions(-) (limited to 'Test/VSI-Benchmarks') 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; - 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 { var head: Node; var tail: Node; - var contents: seq; - var footprint: set; - var spine: set>; + ghost var contents: seq; + ghost var footprint: set; + ghost var spine: set>; function Valid(): bool reads this, footprint; @@ -124,8 +124,8 @@ class Node { var data: T; var next: Node; - var tailContents: seq; - var footprint: set; + ghost var tailContents: seq; + ghost var footprint: set; 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 { - var footprint:set; + ghost var footprint:set; var elements:seq; 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) - 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; call iter.Init(this); @@ -58,49 +58,48 @@ class Iterator { var c:Collection; var pos:int; - var footprint:set; + ghost var footprint:set; 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) - 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; + var c := new Collection; 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 { } class Stream { - var footprint:set; + ghost var footprint:set; var stream:seq; 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) returns (r: Queue, perm:seq); 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; - 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; + 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; + ghost var footprint:set; var isOpen:bool; function Valid():bool @@ -188,7 +188,7 @@ class ReaderStream { } class WriterStream { - var footprint:set; + ghost var footprint:set; var stream:seq; 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 ) -- cgit v1.2.3