From 3baf6dafea70401444ddc94f1b353c3d32a66743 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Fri, 17 Sep 2010 01:26:47 +0000 Subject: 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 --- Test/VSI-Benchmarks/b2.dfy | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'Test/VSI-Benchmarks') 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, 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, 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); -- cgit v1.2.3