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/dafny1 | |
| 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/dafny1')
| -rw-r--r-- | Test/dafny1/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny1/MatrixFun.dfy | 59 | ||||
| -rw-r--r-- | Test/dafny1/runtest.bat | 1 |
3 files changed, 64 insertions, 0 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 71646dab..c81c0268 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -31,6 +31,10 @@ Dafny program verifier finished with 2 verified, 0 errors Dafny program verifier finished with 9 verified, 0 errors
+-------------------- MatrixFun.dfy --------------------
+
+Dafny program verifier finished with 4 verified, 0 errors
+
-------------------- SchorrWaite.dfy --------------------
Dafny program verifier finished with 10 verified, 0 errors
diff --git a/Test/dafny1/MatrixFun.dfy b/Test/dafny1/MatrixFun.dfy new file mode 100644 index 00000000..96d89ad6 --- /dev/null +++ b/Test/dafny1/MatrixFun.dfy @@ -0,0 +1,59 @@ +method MirrorImage<T>(m: array2<T>)
+ requires m != null;
+ modifies m;
+ ensures (forall i,j :: 0 <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==>
+ m[i,j] == old(m[i, m.Length1-1-j]));
+{
+ var a := 0;
+ while (a < m.Length0)
+ invariant a <= m.Length0;
+ invariant (forall i,j :: 0 <= i && i < a && 0 <= j && j < m.Length1 ==>
+ m[i,j] == old(m[i, m.Length1-1-j]));
+ invariant (forall i,j :: a <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==>
+ m[i,j] == old(m[i,j]));
+ {
+ var b := 0;
+ while (b < m.Length1 / 2)
+ invariant b <= m.Length1 / 2;
+ invariant (forall i,j :: 0 <= i && i < a && 0 <= j && j < m.Length1 ==>
+ m[i,j] == old(m[i, m.Length1-1-j]));
+ invariant (forall j :: 0 <= j && j < b ==>
+ m[a,j] == old(m[a, m.Length1-1-j]) &&
+ old(m[a,j]) == m[a, m.Length1-1-j]);
+ invariant (forall j :: b <= j && j < m.Length1-b ==> m[a,j] == old(m[a,j]));
+ invariant (forall i,j :: a+1 <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==>
+ m[i,j] == old(m[i,j]));
+ {
+ var tmp := m[a, m.Length1-1-b];
+ m[a, m.Length1-1-b] := m[a, b];
+ m[a, b] := tmp;
+ b := b + 1;
+ }
+ a := a + 1;
+ }
+}
+
+method Flip<T>(m: array2<T>)
+ requires m != null && m.Length0 == m.Length1;
+ modifies m;
+ ensures (forall i,j :: 0 <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==> m[i,j] == old(m[j,i]));
+{
+ var N := m.Length0;
+ var a := 0;
+ var b := 0;
+ while (a != N)
+ invariant a <= b && b <= N;
+ invariant (forall i,j :: 0 <= i && i <= j && j < N ==>
+ (if i < a || (i == a && j < b)
+ then m[i,j] == old(m[j,i]) && m[j,i] == old(m[i,j])
+ else m[i,j] == old(m[i,j]) && m[j,i] == old(m[j,i])));
+ decreases N-a, N-b;
+ {
+ if (b < N) {
+ var tmp := m[a,b]; m[a,b] := m[b,a]; m[b,a] := tmp;
+ b := b + 1;
+ } else {
+ a := a + 1; b := a;
+ }
+ }
+}
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index eaee07d4..ea5b0ec7 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -16,6 +16,7 @@ for %%f in (Queue.dfy UnboundedStack.dfy
SeparationLogicList.dfy
ListCopy.dfy ListReverse.dfy ListContents.dfy
+ MatrixFun.dfy
SchorrWaite.dfy
SumOfCubes.dfy
TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy
|