diff options
| author |  Rustan Leino <unknown> | 2014-04-04 07:01:32 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-04-04 07:01:32 -0700 |
| commit | 390da153fcba46e4cd511adda888a3920af56862 (patch) | |
| tree | 8c5db48aaed9624a09cab1017c896ae79738fd10 /Test/dafny0/ModifyStmt.dfy | |
| parent | cd206ac033a1e369277f824dd3a13eca32f0396c (diff) | |
Added "modify Frame { Body }" statement.
Diffstat (limited to 'Test/dafny0/ModifyStmt.dfy')
| -rw-r--r-- | Test/dafny0/ModifyStmt.dfy | 59 |
1 files changed, 59 insertions, 0 deletions
diff --git a/Test/dafny0/ModifyStmt.dfy b/Test/dafny0/ModifyStmt.dfy index 49ced294..5e3247ef 100644 --- a/Test/dafny0/ModifyStmt.dfy +++ b/Test/dafny0/ModifyStmt.dfy @@ -158,3 +158,62 @@ class MyClass { }
}
}
+
+class ModifyBody {
+ var x: int;
+ var y: int;
+ method M0()
+ modifies this;
+ {
+ modify {} {
+ x := 3; // error: violates modifies clause of the modify statement
+ }
+ }
+ method M1()
+ modifies this;
+ {
+ modify {} {
+ var o := new ModifyBody;
+ o.x := 3; // fine
+ }
+ }
+ method M2()
+ modifies this;
+ {
+ modify this {
+ x := 3;
+ }
+ }
+ method M3(o: ModifyBody, p: ModifyBody)
+ modifies this, o, p;
+ {
+ modify {this, o, p} {
+ modify this, o;
+ modify o, this {
+ modify o {
+ modify o;
+ modify {} {
+ modify {};
+ }
+ }
+ }
+ }
+ }
+ method P0()
+ modifies this;
+ {
+ var xx := x;
+ modify this;
+ assert xx == x; // error
+ }
+ method P1()
+ modifies this;
+ {
+ var xx := x;
+ modify this {
+ y := 3;
+ }
+ assert xx == x; // fine, because the modify body trumps the modify frame
+ }
+}
+
|