blob: 5987a82bb32c90fd112c052aad289282856bb6e3 (
plain)
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
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
method NinetyOne(x: int, ghost proveFunctionalPostcondition: bool) returns (z: int)
ensures proveFunctionalPostcondition ==> z == if x > 101 then x-10 else 91;
{
var y1 := x;
var y2 := 1;
while (true)
// the following two invariants are needed only to prove the postcondition
invariant proveFunctionalPostcondition ==> 100 < x ==> y1 == x;
invariant proveFunctionalPostcondition ==> x <= 100 < y1 && y2 == 1 ==> y1 == 101;
// the following two lines justify termination, as in the paper by Katz and Manna
invariant (y1 <= 111 && y2 >= 1) || (y1 == x && y2 == 1);
decreases -2*y1 + 21*y2 + 2*(if x < 111 then 111 else x);
{
if (y1 > 100) {
if (y2 == 1) {
break;
} else {
y1 := y1 - 10;
y2 := y2 - 1;
}
} else {
y1 := y1 + 11;
y2 := y2 + 1;
}
}
z := y1 - 10;
}
method Gcd(x1: int, x2: int)
requires 1 <= x1 && 1 <= x2;
{
var y1 := x1;
var y2 := x2;
while (y1 != y2)
invariant 1 <= y1 && 1 <= y2;
decreases y1 + y2;
{
while (y1 > y2)
invariant 1 <= y1 && 1 <= y2;
{
y1 := y1 - y2;
}
while (y2 > y1)
invariant 1 <= y1 && 1 <= y2;
{
y2 := y2 - y1;
}
}
}
method Determinant(X: array2<int>, M: int) returns (z: int)
requires 1 <= M;
requires X != null && M == X.Length0 && M == X.Length1;
modifies X;
{
var y := X[1-1,1-1];
var a := 1;
while (a != M)
invariant 1 <= a <= M;
{
var b := a + 1;
while (b != M+1)
invariant a+1 <= b <= M+1;
{
var c := M;
while (c != a)
invariant a <= c <= M;
{
assume X[a-1,a-1] != 0;
X[b-1, c-1] := X[b-1,c-1] - X[b-1,a-1] / X[a-1,a-1] * X[a-1,c-1];
c := c - 1;
}
b := b + 1;
}
a := a + 1;
y := y * X[a-1,a-1];
}
z := y;
}
|
