diff options
author | 2010-09-17 01:26:47 +0000 | |
---|---|---|
committer | 2010-09-17 01:26:47 +0000 | |
commit | 4744c729d2fa83f324ffa84dc619ad0a321a9c98 (patch) | |
tree | 20f6e9d48144fc0ca96a2db53ee9f0db81e4861f /Test/VSI-Benchmarks/b2.dfy | |
parent | 94087bfa24bd34a5cfcb6c8b361439c6de3135a9 (diff) |
Dafny:
* Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation)
* Changed syntax of array length from |a| to a.Length (for one-dimensional arrays). The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays.
* Internally, this meant adding support for built-in classes and readonly fields
Diffstat (limited to 'Test/VSI-Benchmarks/b2.dfy')
-rw-r--r-- | Test/VSI-Benchmarks/b2.dfy | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy index 1021ee85..6c6f11b3 100644 --- a/Test/VSI-Benchmarks/b2.dfy +++ b/Test/VSI-Benchmarks/b2.dfy @@ -2,18 +2,18 @@ class Benchmark2 {
method BinarySearch(a: array<int>, key: int) returns (result: int)
requires a != null;
- requires (forall i, j :: 0 <= i && i < j && j < |a| ==> a[i] <= a[j]);
- ensures -1 <= result && result < |a|;
+ requires (forall i, j :: 0 <= i && i < j && j < a.Length ==> a[i] <= a[j]);
+ ensures -1 <= result && result < a.Length;
ensures 0 <= result ==> a[result] == key;
- ensures result == -1 ==> (forall i :: 0 <= i && i < |a| ==> a[i] != key);
+ ensures result == -1 ==> (forall i :: 0 <= i && i < a.Length ==> a[i] != key);
{
var low := 0;
- var high := |a|;
+ var high := a.Length;
while (low < high)
- invariant 0 <= low && low <= high && high <= |a|;
+ invariant 0 <= low && low <= high && high <= a.Length;
invariant (forall i :: 0 <= i && i < low ==> a[i] < key);
- invariant (forall i :: high <= i && i < |a| ==> key < a[i]);
+ invariant (forall i :: high <= i && i < a.Length ==> key < a[i]);
{
var mid := low + (high - low) / 2;
var midVal := a[mid];
@@ -49,7 +49,7 @@ method Main() { method TestSearch(a: array<int>, key: int)
requires a != null;
- requires (forall i, j :: 0 <= i && i < j && j < |a| ==> a[i] <= a[j]);
+ requires (forall i, j :: 0 <= i && i < j && j < a.Length ==> a[i] <= a[j]);
{
var b := new Benchmark2;
call r := b.BinarySearch(a, key);
|