diff options
| author |  Rustan Leino <unknown> | 2015-01-27 20:38:55 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-01-27 20:38:55 -0800 |
| commit | 247a2d714e70f8f7be80307f53bdaf7d0033d54e (patch) | |
| tree | 3640cb296281da21d7e502124a55ed2329d161d0 /Test/dafny0/Basics.dfy | |
| parent | cee001acf106fe23e7dd29df4c10c0a2a5293be4 (diff) | |
Assume type properties of values that are created by a havoc assignment. Such assignments are part of assign-such-that statements, and
thus this also fixes Issue 52.
Diffstat (limited to 'Test/dafny0/Basics.dfy')
| -rw-r--r-- | Test/dafny0/Basics.dfy | 120 |
1 files changed, 120 insertions, 0 deletions
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index 26baa35f..c8fa76c8 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -477,3 +477,123 @@ method {:selective_checking} MySelectiveChecking1(x: int, y: int, z: int) }
assert x < z; // error (this doesn't hold if we take the 'then' branch)
}
+
+// ------------- regression test: make sure havoc and assign-such-that statements include type assumptions --
+
+module AssumeTypeAssumptions {
+ predicate f(p: seq<int>)
+
+ method M2() {
+ var path: seq<int>, other: int :| true; // previously, the 2-or-more variable case was broken
+ assume f(path);
+ assert exists path :: f(path);
+ }
+
+ method M1() {
+ var path: seq<int> :| true; // ... whereas the 1-variable case had worked
+ assume f(path);
+ assert exists path :: f(path);
+ }
+
+ method P2() {
+ var path: seq<int>, other: int := *, *;
+ assume f(path);
+ assert exists path :: f(path);
+ }
+
+ method P1() {
+ var path: seq<int> := *;
+ assume f(path);
+ assert exists path :: f(path);
+ }
+
+ method Q2(a: array<seq<int>>, j: int)
+ requires a != null && 0 <= j < a.Length
+ modifies a
+ {
+ var other: int;
+ a[j], other := *, *;
+ assume f(a[j]);
+ assert exists path :: f(path);
+ }
+
+ method Q1(a: array<seq<int>>, j: int)
+ requires a != null && 0 <= j < a.Length
+ modifies a
+ {
+ a[j] := *;
+ assume f(a[j]);
+ assert exists path :: f(path);
+ }
+
+ // -----
+
+ class IntCell {
+ var data: int
+ }
+ class Cell<T> {
+ var data: T
+ }
+
+ method Client_Fixed(x: IntCell)
+ requires x != null
+ modifies x
+ {
+ var xx: int;
+ // regular assignments
+ xx := 7;
+ x.data := 7;
+ // havoc assignments
+ xx := *;
+ x.data := *;
+ }
+
+ method Client_Int(x: Cell<int>, a: array<int>, j: int)
+ requires x != null && a != null && 0 <= j < a.Length
+ modifies x, a
+ {
+ var xx: int;
+ // regular assignments
+ xx := 7;
+ x.data := 7;
+ a[j] := 7;
+ // havoc assignments
+ xx := *;
+ x.data := *;
+ a[j] := *;
+ }
+
+ method Client_U<U>(x: Cell<U>, a: array<U>, j: int, u: U)
+ requires x != null && a != null && 0 <= j < a.Length
+ modifies x, a
+ {
+ var xx: U;
+ // regular assignments
+ xx := u;
+ x.data := u;
+ a[j] := u;
+ // havoc assignments
+ xx := *;
+ x.data := *;
+ a[j] := *;
+ }
+
+ method Client_CellU<U>(x: Cell<Cell<U>>, a: array<Cell<U>>, j: int, u: Cell<U>)
+ requires x != null && a != null && 0 <= j < a.Length
+ modifies x, a
+ {
+ var xx: Cell<U>;
+ // regular assignments
+ xx := u;
+ x.data := u;
+ a[j] := u;
+ // havoc assignments
+ xx := *;
+ x.data := *;
+ a[j] := *;
+ // new assignments
+ xx := new Cell<U>;
+ x.data := new Cell<U>;
+ a[j] := new Cell<U>;
+ }
+}
|