diff options
| author |  Rustan Leino <unknown> | 2014-04-03 18:28:56 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-04-03 18:28:56 -0700 |
| commit | cd206ac033a1e369277f824dd3a13eca32f0396c (patch) | |
| tree | 23f3d5863237de9def3f5c10cb4974dc3191ef14 /Test/dafny0/ModifyStmt.dfy | |
| parent | 7c64906cd2eb3d0258b29e91bdc861743a05ff42 (diff) | |
Added "modify" statement.
In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field.
Diffstat (limited to 'Test/dafny0/ModifyStmt.dfy')
| -rw-r--r-- | Test/dafny0/ModifyStmt.dfy | 160 |
1 files changed, 160 insertions, 0 deletions
diff --git a/Test/dafny0/ModifyStmt.dfy b/Test/dafny0/ModifyStmt.dfy new file mode 100644 index 00000000..49ced294 --- /dev/null +++ b/Test/dafny0/ModifyStmt.dfy @@ -0,0 +1,160 @@ +class MyClass {
+ var x: int;
+ var y: int;
+ ghost var g: int;
+
+ method M(S: set<MyClass>, mc: MyClass)
+ requires this == mc;
+ modifies this, S;
+ {
+ if mc == this {
+ modify mc, this;
+ }
+ modify {this}, this, {this}, S;
+ modify this;
+ modify {:myAttribute} {:another true} {this}, this, S;
+ modify ;
+ }
+
+ method N()
+ modifies this;
+ {
+ x := 18;
+ modify this;
+ assert x == 18; // error: cannot conclude this here
+ }
+
+ method P(other: MyClass)
+ modifies this;
+ {
+ x := 18;
+ var previous := if other == null then 0 else other.x;
+ modify this;
+ assert other != null && other != this ==> other.x == previous;
+ }
+
+ method FieldSpecific0()
+ modifies `x;
+ {
+ modify this; // error: this is a larger frame than what FieldSpecific0 is allowed to modify
+ }
+
+ method FieldSpecific1()
+ modifies `x, `y;
+ {
+ modify this; // error: this is a larger frame than what FieldSpecific0 is allowed to modify
+ }
+
+ method FieldSpecific2()
+ modifies this;
+ {
+ modify `x;
+ }
+
+ method FieldSpecific3()
+ modifies `x;
+ {
+ modify this`x;
+ modify `y; // error: this is a larger frame than what FieldSpecific3 is allowed to modify
+ }
+
+ method FieldSpecific4()
+ modifies `x;
+ {
+ var xx, yy := x, y;
+ modify this`x;
+ assert y == yy; // fine
+ assert x == xx; // error: x just changed
+ }
+
+ ghost method GhostFrame0()
+ modifies `x, `g; // the `x has no effect, since this is a ghost context
+ {
+ modify `x, `g;
+ }
+
+ ghost method GhostFrame1()
+ modifies `g;
+ {
+ modify `x, `g; // the `x has no effect, since this is a ghost context
+ }
+
+ ghost method GhostFrame2()
+ {
+ var xx := x;
+ modify `x; // fine, since we're in a ghost context, so `x doesn't count
+ assert xx == x; // fine
+ }
+
+ method GhostFrame3()
+ {
+ var xx := x;
+ if g < 100 {
+ // we're now in a ghost context
+ modify `x; // fine, since `x doesn't count here
+ }
+ assert xx == x; // fine
+ }
+
+ method GhostFrame4()
+ modifies this;
+ {
+ var xx := x;
+ ghost var gg := g;
+ if g < 100 {
+ // we're now in a ghost context
+ var n := 0;
+ while n < y
+ modifies `x;
+ {
+ if * {
+ g := g + 1; // error: this is an error here, since it violates the loop's modifies clause
+ }
+ n := n + 1;
+ }
+ n := 0;
+ while n < y
+ modifies `x, `g;
+ {
+ g := g + 1;
+ n := n + 1;
+ }
+ }
+ assert x == xx; // fine, since only ghost state is allowed to be modified inside the ghost if
+ assert g == gg; // error
+ }
+
+ ghost method Ghost0()
+ modifies this;
+ {
+ var xx := x;
+ var gg := g;
+ modify this; // since we're in the context of a ghost method, this will only modify ghost fields
+ assert x == xx; // fine
+ assert g == gg; // error
+ }
+
+ ghost method Ghost1()
+ modifies this;
+ {
+ var xx := x;
+ var gg := g;
+ modify `x, `g; // since we're in the context of a ghost method, this will only modify
+ // ghost fields, despite the specific mention of non-ghost fields
+ assert x == xx; // fine
+ assert g == gg; // error
+ }
+
+ method Ghost2()
+ modifies this;
+ {
+ var xx := x;
+ ghost var gg := g;
+ if g < 100 {
+ // the if guard mentions a ghost field, so we're now in a ghost context
+ modify this;
+ assert x == xx; // fine, since the 'modify' statement only modified ghost fields
+ assert g == gg; // error: the 'modify' statement can affect the ghost field 'g'
+ }
+ }
+}
|