1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
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]));
{
m[a, m.Length1-1-b], m[a, b] := m[a, b], m[a, m.Length1-1-b];
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 < m.Length0 && 0 <= j < m.Length1 ==> m[i,j] == old(m[j,i]));
{
var N := m.Length0;
var a := 0;
var b := 1;
while (a != N)
invariant a < b <= N || (a == N && b == N+1);
invariant (forall i,j :: 0 <= i <= 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) {
m[a,b], m[b,a] := m[b,a], m[a,b];
b := b + 1;
} else {
a := a + 1; b := a + 1;
}
}
}
method Main()
{
var B := new bool[2,5];
B[0,0] := true; B[0,1] := false; B[0,2] := false; B[0,3] := true; B[0,4] := false;
B[1,0] := true; B[1,1] := true; B[1,2] := true; B[1,3] := true; B[1,4] := false;
print "Before:\n";
PrintMatrix(B);
MirrorImage(B);
print "Mirror image:\n";
PrintMatrix(B);
var A := new int[3,3];
A[0,0] := 5; A[0,1] := 7; A[0,2] := 9;
A[1,0] := 6; A[1,1] := 2; A[1,2] := 3;
A[2,0] := 7; A[2,1] := 1; A[2,2] := 0;
print "Before:\n";
PrintMatrix(A);
Flip(A);
print "Flip:\n";
PrintMatrix(A);
}
method PrintMatrix<T>(m: array2<T>)
requires m != null;
{
var i := 0;
while (i < m.Length0) {
var j := 0;
while (j < m.Length1) {
print m[i,j];
j := j + 1;
if (j == m.Length1) {
print "\n";
} else {
print ", ";
}
}
i := i + 1;
}
}
|
