diff options
| author |  rustanleino <unknown> | 2010-09-17 01:26:47 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-09-17 01:26:47 +0000 |
| commit | 4744c729d2fa83f324ffa84dc619ad0a321a9c98 (patch) | |
| tree | 20f6e9d48144fc0ca96a2db53ee9f0db81e4861f /Test/dafny0/MultiDimArray.dfy | |
| parent | 94087bfa24bd34a5cfcb6c8b361439c6de3135a9 (diff) | |
Dafny:
* Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation)
* Changed syntax of array length from |a| to a.Length (for one-dimensional arrays). The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays.
* Internally, this meant adding support for built-in classes and readonly fields
Diffstat (limited to 'Test/dafny0/MultiDimArray.dfy')
| -rw-r--r-- | Test/dafny0/MultiDimArray.dfy | 91 |
1 files changed, 91 insertions, 0 deletions
diff --git a/Test/dafny0/MultiDimArray.dfy b/Test/dafny0/MultiDimArray.dfy new file mode 100644 index 00000000..ba5dc9da --- /dev/null +++ b/Test/dafny0/MultiDimArray.dfy @@ -0,0 +1,91 @@ +class A {
+ // all of the following array types are allowed
+ var a: array<int>;
+ var b: array <bool>;
+ var c: array <A>;
+ var d: array1 <A>; // this is a synonym for array<A>
+ var e: array2 <A>;
+ var f: array3 <A>;
+ var g: array300 <A>;
+ var h: array3000 <array2<int>>;
+
+ method M0()
+ requires a != null && b != null;
+ modifies a;
+ {
+ if (5 <= a.Length && a.Length <= b.Length) {
+ var x := b[2];
+ var y := a[1];
+ var z := a[2];
+ a[2] := a[2] + 1;
+ assert x == b[2];
+ assert y == a[1];
+ assert z == a[2] - 1;
+ }
+ }
+
+ method M1()
+ requires a != null && d != null;
+ modifies a;
+ {
+ if (5 <= a.Length && a.Length <= d.Length) {
+ var x := d[2];
+ var y := a[1];
+ var z := a[2];
+ a[2] := a[2] + 1;
+ assert y == a[1];
+ assert z == a[2] - 1;
+ assert x == d[2]; // error: a and d may be equal
+ }
+ }
+
+ method M2(i: int, j: int, k: int, val: A)
+ requires f != null;
+ requires 0 <= i && i < f.Length0;
+ requires 0 <= j && j < f.Length1;
+ requires 0 <= k && k < f.Length2;
+ modifies f;
+ {
+ if (*) {
+ if (k < f.Length0) {
+ var save := f[k,j,k];
+ f[i,j,k] := val;
+ assert save == f[k,j,k]; // error: k and i may be equal
+ }
+ } else if (k < f.Length0 && k != i) {
+ if (k < f.Length0) {
+ var save := f[k,j,k];
+ f[i,j,k] := val;
+ assert save == f[k,j,k]; // fine
+ }
+ }
+ }
+
+ method M3(i: int, j: int, k: int)
+ requires f != null;
+ requires 0 <= i && i < f.Length0;
+ requires 0 <= j && j < f.Length1;
+ requires 0 <= k && k < f.Length2;
+ modifies f;
+ decreases i;
+ {
+ if (i != 0) {
+ var z := new A[2,3,5]; // first three primes (nice!)
+ var s := z[1,2,4]; // first three powers of 2 (tra-la-la)
+ var some: A;
+ f[i,j,k] := some;
+ call M3(i-1, j, k);
+ assert s == z[1,2,4];
+ if (*) {
+ assert f[i,j,k] == some; // error: the recursive call may have modified any element in 'f'
+ }
+ }
+ }
+
+ method M4(a: array2<bool>) returns (k: int)
+ requires a != null;
+ ensures 0 <= k;
+ {
+ k := a.Length0 + a.Length1;
+ }
+}
|