diff options
author | 2010-05-06 20:28:29 +0000 | |
---|---|---|
committer | 2010-05-06 20:28:29 +0000 | |
commit | a2f70f46e1a4dfb513df45657178399269cec67d (patch) | |
tree | bacc4d411170492170faa80fd619a009da602650 /Test/VSI-Benchmarks/b2.dfy | |
parent | e9c25e761ad3a5e31e077f7bb595bfc10618c2bb (diff) |
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
Diffstat (limited to 'Test/VSI-Benchmarks/b2.dfy')
-rw-r--r-- | Test/VSI-Benchmarks/b2.dfy | 53 |
1 files changed, 49 insertions, 4 deletions
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";
}
+******/
|