diff options
Diffstat (limited to 'Test/dafny0/Array.dfy')
| -rw-r--r-- | Test/dafny0/Array.dfy | 255 |
1 files changed, 0 insertions, 255 deletions
diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy deleted file mode 100644 index d8bffce4..00000000 --- a/Test/dafny0/Array.dfy +++ /dev/null @@ -1,255 +0,0 @@ -class A {
- method M() {
- var y := new A[100];
- y[5] := null;
- }
-
- method N0() {
- var a: array<int>;
- if (a != null && 5 < a.Length) {
- a[5] := 12; // error: violates modifies clause
- }
- }
-
- method N1(a: array<int>)
- modifies a;
- {
- var b := a.Length; // 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.Length;
- modifies a;
- ensures (forall i :: 0 <= i && i < a.Length ==> 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
- var o: object := zz0;
- assert this != o; // holds because zz0 has a different type
- /****** This would be a good thing to be able to verify, but the current encoding is not up to the task
- if (zz0 != null && zz1 != null && 2 <= zz0.Length && zz0.Length == zz1.Length) {
- 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.Length) {
- x[5] := 12; // error: violates modifies clause
- }
- }
- method P1()
- modifies this`x;
- {
- if (x != null && 100 <= x.Length) {
- x[5] := 12; // error: violates modifies clause
- }
- }
- method P2()
- modifies x;
- {
- if (x != null && 100 <= x.Length) {
- x[5] := 12; // fine
- }
- }
-
- method Q() {
- var a := new int[5];
- a[0],a[1],a[2],a[3],a[4] := 0,1,2,3,4;
-
- assert [1,2,3,4] == a[1..];
- assert [1,2,3,4] == a[1.. a.Length];
- assert [1] == a[1..2];
- assert [0,1] == a[..2];
- assert [0,1] == a[0..2];
- assert forall i :: 0 <= i <= a.Length ==> [] == a[i..i];
- assert [0,1,2,3,4] == a[..];
- assert forall i :: 0 <= i < a.Length ==> a[i] == i;
- }
-
- method ArrayToSequenceTests(a: array<int>, lo: int, hi: int)
- requires a != null;
- {
- if (a.Length == 10) {
- var s;
- s := a[2..5];
- assert |s| == 3;
- s := a[..5];
- assert |s| == 5;
- s := a[2..];
- assert |s| == 8;
- s := a[..];
- assert |s| == 10;
- s := a[..10] + a[0..];
- } else {
- if {
- case 0 <= lo <= a.Length =>
- var s := a[lo..] + a[..lo];
- case 0 <= lo <= a.Length && 0 <= hi <= a.Length =>
- var s := a[lo..hi]; // error: lo may be greater than hi
- case true =>
- }
- }
- }
-
- function BadRangeReads(a: array<int>, all: bool): bool
- {
- a != null && a.Length == 10 &&
- if all then
- a[..] == [] // error: not allowed to read the elements of a
- else
- a[2..5] + // error: not allowed to read the elements of a
- a[..5] + // error: not allowed to read the elements of a
- a[2..] == [] // error: not allowed to read the elements of a
- }
- function GoodRangeReads(a: array<int>, all: bool): bool
- reads a;
- {
- a != null && a.Length == 10 &&
- if all then
- a[..] == [] // no prob, since we now have a reads clause
- else
- a[2..5] + a[..5] + a[2..] == [] // no prob, since we now have a reads clause
- }
- function AnotherGoodRangeReads(a: array<int>, j: int): bool
- {
- a != null && 0 <= j && j <= a.Length &&
- a[j..j] == []
- }
-}
-
-type B;
-
-// -------------------------------
-
-class ArrayTests {
- function F0(a: array<int>): bool
- {
- a != null && 10 <= a.Length &&
- a[7] == 13 // error: reads on something outside reads clause
- }
-
- var b: array<int>;
- function F1(): bool
- reads this;
- {
- b != null && 10 <= b.Length &&
- b[7] == 13 // error: reads on something outside reads clause
- }
-
- function F2(a: array<int>): bool
- reads this, b, a;
- {
- a != null && 10 <= a.Length &&
- a[7] == 13 // good
- &&
- b != null && 10 <= b.Length &&
- b[7] == 13 // good
- }
-
- method M0(a: array<int>)
- requires a != null && 10 <= a.Length;
- {
- a[7] := 13; // error: updates location not in modifies clause
- }
-
- method M1()
- requires b != null && 10 <= b.Length;
- 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.Length;
- requires b != null && 10 <= b.Length;
- modifies this, b, a;
- {
- a[7] := 13; // good
- b[7] := 13; // good
- }
-}
-
-// -------------------- induction attribute --------------------------------
-
-ghost method Fill_I(s: seq<int>)
- requires forall i :: 1 <= i < |s| ==> s[i-1] <= s[i];
- ensures forall i,j {:induction i} :: 0 <= i < j < |s| ==> s[i] <= s[j];
-{ // error: cannot prove postcondition
-}
-
-ghost method Fill_J(s: seq<int>)
- requires forall i :: 1 <= i < |s| ==> s[i-1] <= s[i];
- ensures forall i,j {:induction j} :: 0 <= i < j < |s| ==> s[i] <= s[j];
-{
-}
-
-ghost method Fill_All(s: seq<int>)
- requires forall i :: 1 <= i < |s| ==> s[i-1] <= s[i];
- ensures forall i,j {:induction i,j} :: 0 <= i < j < |s| ==> s[i] <= s[j];
-{
-}
-
-ghost method Fill_True(s: seq<int>)
- requires forall i :: 1 <= i < |s| ==> s[i-1] <= s[i];
- ensures forall i,j {:induction} :: 0 <= i < j < |s| ==> s[i] <= s[j];
-{
-}
-
-ghost method Fill_False(s: seq<int>)
- requires forall i :: 1 <= i < |s| ==> s[i-1] <= s[i];
- ensures forall i,j {:induction false} :: 0 <= i < j < |s| ==> s[i] <= s[j];
-{ // error: cannot prove postcondition
-}
-
-ghost method Fill_None(s: seq<int>)
- requires forall i :: 1 <= i < |s| ==> s[i-1] <= s[i];
- ensures forall i,j :: 0 <= i < j < |s| ==> s[i] <= s[j];
-{ // error: cannot prove postcondition
-}
-
-// -------------- some regression tests; there was a time when array-element LHSs of calls were not translated correctly
-
-method Test_ArrayElementLhsOfCall(a: array<int>, i: int, c: Cdefg<int>) returns (x: int)
- requires a != null && c != null;
- modifies a, c;
-{
- if (0 <= i < a.Length) {
- a[i] := x;
- a[i] := Test_ArrayElementLhsOfCall(a, i-1, c); // this line used to crash Dafny
- c.t := x;
- c.t := Test_ArrayElementLhsOfCall(a, i-1, c); // this line used to crash Dafny
- var n: nat;
- n := x; // error: subrange check is applied and it cannot be verified
- n := Test_ArrayElementLhsOfCall(a, i-1, c); // error: subrange check is applied and it cannot be verified
- }
-}
-
-class Cdefg<T> {
- var t: T;
-}
|