diff options
Diffstat (limited to 'Test/dafny4')
| -rw-r--r-- | Test/dafny4/BinarySearch.dfy | 36 |
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] {
|