blob: 96561ebd97de16d5d9e221b99781e5957206de67 (
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
|
function SimpleAssert(n: int): int
ensures n < 100;
{
assert n == 58; // error: assert violation
n // but postcondition is fine
}
function SimpleAssume(n: int): int
ensures n < 100;
{
assume n == 58; n // all is fine
}
function Subonacci(n: nat): nat
{
if 2 <= n then
// proving that this case is a nat requires more information,
// which is here supplied by an assume expression
assume Subonacci(n-2) <= Subonacci(n-1);
Subonacci(n-1) - Subonacci(n-2)
else
n
}
function F(n: int): nat
{
Subonacci(assume 0 <= n; n) -
Subonacci(n)
}
function G(n: int, b: bool): nat
{
if b then
Subonacci(assume 0 <= n; n) + n // the last n is also affected by the assume
else
Subonacci(n) // error: n may not be a nat
}
ghost method M(m: nat, n: int)
{
var k := F(m);
assert k == 0;
k := F(n);
assert k == 0; // this is still known
}
method M0(j: int) returns (n: nat)
{
n := assert 0 <= j; j; // error: j may be negative
}
method M1(j: int) returns (n: nat)
{
n := (assume 0 <= j; j) + (assert 0 <= j; j);
assert n == 2*j;
}
function SpecOnly(): bool { true }
function method FuncMeth(): int {
assert SpecOnly(); // this call is allowed, because the .Guard of a
// PredicateExpr is not included in compilation
15
}
method M5(a: int, b: int)
{
var k := if a < 0 then
assume b < 0; 5
else
5;
if (*) {
assert a == -7 ==> b < 0;
assert b < 0; // error: this condition does not hold on every path here
} else {
assert assume a == -7; b < 0; // note, this is different than the ==> above
assert b < 0; // this condition does hold on all paths to here
}
}
|
