diff options
author | 2009-10-30 23:52:13 +0000 | |
---|---|---|
committer | 2009-10-30 23:52:13 +0000 | |
commit | 1b9369b6ea837aeeb932733cdb7178f5113a042c (patch) | |
tree | 0782b3ab89221889f5bda986d02f52ae1c4e4254 /Test/VSI-Benchmarks/b2.dfy | |
parent | 5eee5f136a9296a0e3178f5d1d564c0241352dc4 (diff) |
Initial version of VSI Benchmarks 1 - 8
Diffstat (limited to 'Test/VSI-Benchmarks/b2.dfy')
-rw-r--r-- | Test/VSI-Benchmarks/b2.dfy | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy new file mode 100644 index 00000000..53eb49a8 --- /dev/null +++ b/Test/VSI-Benchmarks/b2.dfy @@ -0,0 +1,60 @@ +
+// 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 {
+ method BinarySearch(a: Array, key: int) returns (result: int)
+ requires a != null;
+ requires (forall i, j ::
+ 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));
+ ensures -1 <= result && result < a.Length();
+ ensures 0 <= result ==> a.Get(result) == key;
+ ensures result == -1 ==>
+ (forall i :: 0 <= i && i < a.Length() ==> a.Get(i) != key);
+ {
+ var low := 0;
+ var high := a.Length();
+
+ while (low < high)
+ invariant 0 <= low && high <= a.Length();
+ invariant (forall i :: 0 <= i && i < low ==> a.Get(i) < key);
+ invariant (forall i :: high <= i && i < a.Length() ==> key < a.Get(i));
+ decreases high - low;
+ {
+ var mid := low + (high - low) / 2;
+ var midVal := a.Get(mid);
+
+ if (midVal < key) {
+ low := mid + 1;
+ } else if (key < midVal) {
+ high := mid;
+ } else {
+ result := mid; // key found
+ return;
+ }
+ }
+ result := -1; // key not present
+ }
+}
+
+class Array {
+ var contents: seq<int>;
+ method Init(n: int);
+ requires 0 <= n;
+ modifies this;
+ ensures |contents| == n;
+ function Length(): int
+ reads this;
+ { |contents| }
+ function Get(i: int): int
+ requires 0 <= i && i < |contents|;
+ reads this;
+ { contents[i] }
+ method Set(i: int, x: int);
+ requires 0 <= i && i < |contents|;
+ modifies this;
+ ensures contents[..i] == old(contents[..i]);
+ ensures contents[i] == x;
+ ensures contents[i+1..] == old(contents[i+1..]);
+}
|