diff options
| author |  rustanleino <unknown> | 2010-05-21 18:38:47 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-05-21 18:38:47 +0000 |
| commit | 572b11dddba3bfbdc4e90beb4d7f2e076878f717 (patch) | |
| tree | 421f92d259589f7711ee1a13b58529dd59d066c6 /Test/dafny0/Array.dfy | |
| parent | 425a4c8ff53eb2196e684b6843016baadfe60835 (diff) | |
Dafny:
* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks
Diffstat (limited to 'Test/dafny0/Array.dfy')
| -rw-r--r-- | Test/dafny0/Array.dfy | 156 |
1 files changed, 156 insertions, 0 deletions
diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy new file mode 100644 index 00000000..928f2bc5 --- /dev/null +++ b/Test/dafny0/Array.dfy @@ -0,0 +1,156 @@ +class A {
+ method M() {
+ var y := new A[100];
+ y[5] := null;
+ }
+
+ method N0() {
+ var a;
+ if (a != null && 5 < |a|) {
+ a[5] := 12; // error: violates modifies clause
+ }
+ }
+
+ method N1(a: array<int>)
+ modifies a;
+ {
+ var b := |a|; // error: a may be null
+ }
+
+ method N2(a: array<int>)
+ requires a != null;
+ modifies a;
+ {
+ a[5] := 12; // error: index may be outside bounds
+ }
+
+ method N3(a: array<int>)
+ requires a != null && 5 < |a|;
+ modifies a;
+ ensures (forall i :: 0 <= i && i < |a| ==> a[i] == old(a[i]) || (i == 5 && a[i] == 12));
+ {
+ a[5] := 12; // all is good
+ }
+
+ var zz0: array<A>;
+ var zz1: array<B>;
+ method O() {
+ var zz2 := new A[25];
+ assert zz2 != zz0; // holds because zz2 is newly allocated
+ /****** These would be good things to be able to verify, but the current encoding is not up to the task
+ var o: object := zz0;
+ assert this != o; // holds because zz0 has a different type
+ if (zz0 != null && zz1 != null && 2 <= |zz0| && |zz0| == |zz1|) {
+ o := zz1[1];
+ assert zz0[1] == o ==> o == null; // holds because zz0 and zz1 have different element types
+ }
+ ******/
+ assert zz2[20] == null; // error: no reason that this must hold
+ }
+
+ var x: array<int>;
+ method P0()
+ modifies this;
+ {
+ if (x != null && 100 <= |x|) {
+ x[5] := 12; // error: violates modifies clause
+ }
+ }
+ method P1()
+ modifies this`x;
+ {
+ if (x != null && 100 <= |x|) {
+ x[5] := 12; // error: violates modifies clause
+ }
+ }
+ method P2()
+ modifies x;
+ {
+ if (x != null && 100 <= |x|) {
+ x[5] := 12; // fine
+ }
+ }
+
+ method Q() {
+ var y := new object[100];
+ y[5] := null;
+ y[0..] := null;
+ y[..83] := null;
+ y[0..|y|] := null;
+ }
+
+ method R() {
+ var y := new int[100];
+ y[55] := 80;
+ y[10..] := 25;
+ y[..83] := 30;
+ y[50..60] := 35;
+ y[55] := 90;
+
+ assert y[54] == 35;
+ assert y[55] == 90;
+ assert y[83] == 25;
+ assert y[8] == 30;
+ assert y[90] + y[91] + y[0] + 20 == |y|;
+ assert y[93] == 24; // error (it's 25)
+ }
+}
+
+class B { }
+
+// -------------------------------
+
+class ArrayTests {
+ function F0(a: array<int>): bool
+ {
+ a != null && 10 <= |a| &&
+ a[7] == 13 // error: reads on something outside reads clause
+ }
+
+ var b: array<int>;
+ function F1(): bool
+ reads this;
+ {
+ b != null && 10 <= |b| &&
+ b[7] == 13 // error: reads on something outside reads clause
+ }
+
+ function F2(a: array<int>): bool
+ reads this, b, a;
+ {
+ a != null && 10 <= |a| &&
+ a[7] == 13 // good
+ &&
+ b != null && 10 <= |b| &&
+ b[7] == 13 // good
+ }
+
+ method M0(a: array<int>)
+ requires a != null && 10 <= |a|;
+ {
+ a[7] := 13; // error: updates location not in modifies clause
+ }
+
+ method M1()
+ requires b != null && 10 <= |b|;
+ modifies this;
+ {
+ b[7] := 13; // error: updates location not in modifies clause
+ }
+
+ method M2()
+ modifies this;
+ {
+ var bb := new int[75];
+ b := bb; // fine
+ }
+
+ method M3(a: array<int>)
+ requires a != null && 10 <= |a|;
+ requires b != null && 10 <= |b|;
+ modifies this, b, a;
+ {
+ a[7] := 13; // good
+ b[7] := 13; // good
+ }
+}
|