Made semi-colons are specification clauses optional. In a future version, they will no longer be allowed.

1 files changed, 18 insertions, 18 deletions

diff --git a/Test/dafny4/BinarySearch.dfy b/Test/dafny4/BinarySearch.dfy
index 1c1d7299..b11fc0d1 100644
--- a/Test/dafny4/BinarySearch.dfy
+++ b/Test/dafny4/BinarySearch.dfy
@@ -4,15 +4,15 @@
 // Binary search using standard integers

 

 method BinarySearch(a: array<int>, key: int) returns (r: int)

-  requires a != null;

-  requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j];

-  ensures 0 <= r ==> r < a.Length && a[r] == key;

-  ensures r < 0 ==> key !in a[..];

+  requires a != null

+  requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]

+  ensures 0 <= r ==> r < a.Length && a[r] == key

+  ensures r < 0 ==> key !in a[..]

 {

   var lo, hi := 0, a.Length;

   while lo < hi

-    invariant 0 <= lo <= hi <= a.Length;

-    invariant key !in a[..lo] && key !in a[hi..];

+    invariant 0 <= lo <= hi <= a.Length

+    invariant key !in a[..lo] && key !in a[hi..]

   {

     var mid := (lo + hi) / 2;

     if key < a[mid] {

@@ -31,15 +31,15 @@ method BinarySearch(a: array<int>, key: int) returns (r: int)
 newtype int32 = x | -0x8000_0000 <= x < 0x8000_0000

 

 method BinarySearchInt32_bad(a: array<int>, key: int) returns (r: int32)

-  requires a != null && a.Length < 0x8000_0000;

-  requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j];

-  ensures 0 <= r ==> r < int32(a.Length) && a[r] == key;

-  ensures r < 0 ==> key !in a[..];

+  requires a != null && a.Length < 0x8000_0000

+  requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]

+  ensures 0 <= r ==> r < int32(a.Length) && a[r] == key

+  ensures r < 0 ==> key !in a[..]

 {

   var lo, hi := 0, int32(a.Length);

   while lo < hi

-    invariant 0 <= lo <= hi <= int32(a.Length);

-    invariant key !in a[..lo] && key !in a[hi..];

+    invariant 0 <= lo <= hi <= int32(a.Length)

+    invariant key !in a[..lo] && key !in a[hi..]

   {

     var mid := (lo + hi) / 2;  // error: possible overflow

     if key < a[mid] {

@@ -54,15 +54,15 @@ method BinarySearchInt32_bad(a: array<int>, key: int) returns (r: int32)
 }

 

 method BinarySearchInt32_good(a: array<int>, key: int) returns (r: int32)

-  requires a != null && a.Length < 0x8000_0000;

-  requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j];

-  ensures 0 <= r ==> r < int32(a.Length) && a[r] == key;

-  ensures r < 0 ==> key !in a[..];

+  requires a != null && a.Length < 0x8000_0000

+  requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]

+  ensures 0 <= r ==> r < int32(a.Length) && a[r] == key

+  ensures r < 0 ==> key !in a[..]

 {

   var lo, hi := 0, int32(a.Length);

   while lo < hi

-    invariant 0 <= lo <= hi <= int32(a.Length);

-    invariant key !in a[..lo] && key !in a[hi..];

+    invariant 0 <= lo <= hi <= int32(a.Length)

+    invariant key !in a[..lo] && key !in a[hi..]

   {

     var mid := lo + (hi - lo) / 2;  // this is how to do it

     if key < a[mid] {