diff options
| author |  leino <unknown> | 2014-10-21 14:39:02 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-21 14:39:02 -0700 |
| commit | e94dc5817a729ebdd6786deb17e1903974c8b981 (patch) | |
| tree | a9fd620cd9af4447c59e4d20c7adc61c48864e04 /Test/dafny4/BinarySearch.dfy | |
| parent | e72bc10129c6cef993f40fba751ff22260410c21 (diff) | |
Fixed crash in inferred descreases clauses involving newtypes.
Added BinarySearch as a test case.
Diffstat (limited to 'Test/dafny4/BinarySearch.dfy')
| -rw-r--r-- | Test/dafny4/BinarySearch.dfy | 77 |
1 files changed, 77 insertions, 0 deletions
diff --git a/Test/dafny4/BinarySearch.dfy b/Test/dafny4/BinarySearch.dfy new file mode 100644 index 00000000..a06f6c4a --- /dev/null +++ b/Test/dafny4/BinarySearch.dfy @@ -0,0 +1,77 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// 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[..];
+{
+ var lo, hi := 0, a.Length;
+ while lo < 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] {
+ hi := mid;
+ } else if a[mid] < key {
+ lo := mid + 1;
+ } else {
+ return mid;
+ }
+ }
+ return -1;
+}
+
+// Binary search using bounded integers
+
+newtype int32 = x | -0x80000000 <= x < 0x80000000
+
+method BinarySearchInt32_bad(a: array<int>, key: int) returns (r: int32)
+ requires a != null && a.Length < 0x80000000;
+ 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..];
+ {
+ var mid := (lo + hi) / 2; // error: possible overflow
+ if key < a[mid] {
+ hi := mid;
+ } else if a[mid] < key {
+ lo := mid + 1;
+ } else {
+ return mid;
+ }
+ }
+ return -1;
+}
+
+method BinarySearchInt32_good(a: array<int>, key: int) returns (r: int32)
+ requires a != null && a.Length < 0x80000000;
+ 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..];
+ {
+ var mid := lo + (hi - lo) / 2; // this is how to do it
+ if key < a[mid] {
+ hi := mid;
+ } else if a[mid] < key {
+ lo := mid + 1;
+ } else {
+ return mid;
+ }
+ }
+ return -1;
+}
|