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

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);