diff options
| author |  chmaria <unknown> | 2014-11-06 07:33:24 +0100 |
|---|---|---|
| committer | chmaria <unknown> | 2014-11-06 07:33:24 +0100 |
| commit | c98ea1bb268730f8b6dc219be4f93f146b3786ca (patch) | |
| tree | 5cc1a2cc73674c2506002f11fa687f87145b8e63 /Test/dafny0/DirtyLoops.dfy | |
| parent | ae0982daf944f7e79fc6b8d73afd1f62f943d7ed (diff) | |
Added computation of free variables in dirty while statements.
Diffstat (limited to 'Test/dafny0/DirtyLoops.dfy')
| -rw-r--r-- | Test/dafny0/DirtyLoops.dfy | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/Test/dafny0/DirtyLoops.dfy b/Test/dafny0/DirtyLoops.dfy index d3164fa9..b283756b 100644 --- a/Test/dafny0/DirtyLoops.dfy +++ b/Test/dafny0/DirtyLoops.dfy @@ -19,3 +19,15 @@ method M2(x: int) invariant i <= x;
decreases i;
}
+
+var f: int;
+
+method M3(x: int)
+ requires f <= x;
+ modifies `f;
+{
+ while (0 < f)
+ invariant f <= x;
+ decreases f;
+ modifies `f;
+}
|