diff options
| author |  Jason Koenig <unknown> | 2011-06-29 11:00:53 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-06-29 11:00:53 -0700 |
| commit | 5a0db96c13bea139372e1c5ad118065678821f2c (patch) | |
| tree | b6f861a1f193c059023da21e39a19c89ec0c53c5 /Test | |
| parent | 7c04533b29ae44bd9be02a4e03a6cf7eb8bd3b7d (diff) | |
Added regression test file LoopModifies.dfy.
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/LoopModifies.dfy | 293 |
1 files changed, 293 insertions, 0 deletions
diff --git a/Test/dafny0/LoopModifies.dfy b/Test/dafny0/LoopModifies.dfy new file mode 100644 index 00000000..17a4228e --- /dev/null +++ b/Test/dafny0/LoopModifies.dfy @@ -0,0 +1,293 @@ +
+// regular modifies sanity test:
+method Testing1(a: array<int>)
+ requires a != null && a.Length > 0;
+{
+ a[0] := 0;
+}
+
+// array inside while loop, without explict modifies clause:
+method Testing2(a: array<int>)
+ requires a != null && a.Length > 0;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ {
+ a[0] := i;
+ i := i + 1;
+ }
+}
+
+// array inside while loop, without explict modifies clause:
+method Testing2A(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies a;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ {
+ // now there is no problem.
+ a[0] := i;
+ i := i + 1;
+ }
+}
+
+// array inside while loop, with explict modifies clause:
+method Testing3(a: array<int>)
+ requires a != null && a.Length > 0;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies;
+ {
+ a[0] := i;
+ i := i + 1;
+ }
+}
+
+// modifies restricts:
+method Testing4(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies a;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies;
+ {
+ a[0] := i;
+ i := i + 1;
+ }
+ // should be ok.
+ a[0] := 1;
+}
+
+// modifies not a subset:
+method Testing5(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a;
+ {
+ a[0] := i;
+ i := i + 1;
+ }
+}
+
+// modifies is a subset, but modifications occur outside:
+method Testing6(a: array<int>, b: array<int>)
+ requires a != null && a.Length > 0;
+ requires b != null && b.Length > 0;
+ modifies a, b;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a;
+ {
+ // cool.
+ a[0] := i;
+
+ // not cool.
+ b[0] := i;
+ i := i + 1;
+ }
+}
+
+// heap outside modifies is actually preserved:
+method Testing7(a: array<int>, b: array<int>)
+ requires a != null && a.Length > 0;
+ requires b != null && b.Length > 0;
+ requires a != b;
+ modifies a, b;
+{
+ var i := 0;
+ b[0] := 4;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a;
+ {
+ // still good.
+ a[0] := i;
+ i := i + 1;
+ }
+ // this is new, and good:
+ assert b[0] == 4;
+}
+
+// modifies actually restrict frame when nested:
+method Testing8(a: array<int>, b: array<int>, c: array<int>)
+ requires a != null && a.Length > 0;
+ requires b != null && b.Length > 0;
+ requires c != null && c.Length > 0;
+ requires a != b && b != c && c != a;
+ modifies a, b, c;
+{
+ var i := 0;
+ b[0] := 4;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a, b;
+ {
+ var j := 0;
+ while(j < 10)
+ invariant 0 <= j <= 10;
+ modifies a;
+ {
+ // happy:
+ a[0] := j;
+ // not happy:
+ b[0] := i;
+ j := j + 1;
+ }
+ i := i + 1;
+ }
+ c[0] := 1;
+}
+
+// heap outside modifies preserved when nested:
+method Testing9(a: array<int>, b: array<int>, c: array<int>)
+ requires a != null && a.Length > 0;
+ requires b != null && b.Length > 0;
+ requires c != null && c.Length > 0;
+ requires a != b && b != c && c != a;
+ modifies a, b, c;
+{
+ var i := 0;
+ b[0] := 4;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a, b;
+ {
+ var j := 0;
+ b[0] := i;
+ while(j < 10)
+ invariant 0 <= j <= 10;
+ modifies a;
+ {
+ a[0] := j;
+ j := j + 1;
+ }
+ assert b[0] == i;
+ i := i + 1;
+ }
+ c[0] := 1;
+}
+
+// allocation, fresh tests:
+
+// allocated things not automatically in modifies of loops:
+method Testing10(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies a;
+{
+ var i := 0;
+ var arr := new int[1];
+ arr[0] := 1; // good, even though not in method modifies.
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a;
+ {
+ arr[0] := 1; // bad.
+ i := i + 1;
+ }
+}
+
+// unless no modifies given, in which case the context is used:
+method Testing10a(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies a;
+{
+ var i := 0;
+ var arr := new int[1];
+ arr[0] := 1; // still good.
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ {
+ arr[0] := 1; // no modifies, so allowed to touch arr.
+ i := i + 1;
+ }
+}
+
+// arr still accessible after loop that can't touch it.
+method Testing11()
+{
+ var i := 0;
+ var arr := new int[1];
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies;
+ {
+ arr := new int[1];
+ arr[0] := 1;
+ var j := 0;
+ while(j < 10)
+ invariant 0 <= j <= 10;
+ modifies;
+ {
+ // can't touch arr in here.
+ j := j + 1;
+ }
+ arr[0] := 2;
+ i := i + 1;
+ }
+}
+
+// allocation inside a loop is still ok:
+method Testing11a(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies a;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a;
+ {
+ var arr := new int[1];
+ arr[0] := 1; // can modify arr, even though it
+ // is not in modifies because it is fresh.
+ var j := 0;
+ while(j < 10)
+ invariant 0 <= j <= 10;
+ modifies a;
+ {
+ arr[0] := 3; // can't touch arr, as allocated before modifies captured.
+ j := j + 1;
+ }
+ i := i + 1;
+ }
+}
+
+class Elem
+{
+ var i: int;
+}
+
+// capture of modifies clause at beginning of loop:
+method Testing12(a: Elem, b: Elem, c: Elem)
+ requires a != null && b != null && c != null;
+ requires a != b && b != c && c != a; // all different.
+ modifies a, b, c;
+{
+ var i := 0;
+ var S := {a, b, c};
+ // S "captured" here for purposes of modifies clause.
+ while(S != {})
+ modifies S;
+ decreases S;
+ {
+ var j := choose S;
+ // these still good, even though S shrinks to not include them.
+ a.i := i;
+ b.i := i;
+ c.i := i;
+ S := S - {j};
+ i := i + 1;
+ }
+}
\ No newline at end of file |