diff options
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 5 | ||||
| -rw-r--r-- | Test/dafny4/BinarySearch.dfy | 77 | ||||
| -rw-r--r-- | Test/dafny4/BinarySearch.dfy.expect | 9 |
3 files changed, 90 insertions, 1 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 834e6aba..c328f7b7 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -392,6 +392,7 @@ namespace Microsoft.Dafny { return t.IsIntegerType || t.IsRealType || t.AsNewtype != null;
}
public enum NumericPersuation { Int, Real }
+ [Pure]
public bool IsNumericBased(NumericPersuation p) {
Type t = this;
while (true) {
@@ -4758,7 +4759,9 @@ namespace Microsoft.Dafny { public static Expression CreateSubtract(Expression e0, Expression e1) {
Contract.Requires(e0 != null);
Contract.Requires(e1 != null);
- Contract.Requires((e0.Type.NormalizeExpand() is IntType && e1.Type.NormalizeExpand() is IntType) || (e0.Type.NormalizeExpand() is RealType && e1.Type.NormalizeExpand() is RealType));
+ Contract.Requires(
+ (e0.Type.IsNumericBased(Type.NumericPersuation.Int) && e1.Type.IsNumericBased(Type.NumericPersuation.Int)) ||
+ (e0.Type.IsNumericBased(Type.NumericPersuation.Real) && e1.Type.IsNumericBased(Type.NumericPersuation.Real)));
Contract.Ensures(Contract.Result<Expression>() != null);
var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Sub, e0, e1);
s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub; // resolve here
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;
+}
diff --git a/Test/dafny4/BinarySearch.dfy.expect b/Test/dafny4/BinarySearch.dfy.expect new file mode 100644 index 00000000..944f677a --- /dev/null +++ b/Test/dafny4/BinarySearch.dfy.expect @@ -0,0 +1,9 @@ +BinarySearch.dfy(44,20): Error: result of operation might violate newtype constraint
+Execution trace:
+ (0,0): anon0
+ BinarySearch.dfy(40,3): anon18_LoopHead
+ (0,0): anon18_LoopBody
+ BinarySearch.dfy(40,3): anon19_Else
+ BinarySearch.dfy(40,3): anon23_Else
+
+Dafny program verifier finished with 6 verified, 1 error
|