blob: 97fcfccb173c6a9f73e86913a590affa77ecc538 (
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
|
method M(x: int)
{ assert x < 20 || 10 <= x; // always true
assert x < 10; // error
Other(x); // error: precondition violation
}
method Other(y: int)
requires 0 <= y
{
}
method Posty() returns (z: int)
ensures 2 <= z // error: postcondition violation
{
var t := 20;
if t < z {
} else { // the postcondition violation occurs on this 'else' branch
}
}
method NoChangeWhazzoeva(u: int)
{
assert u != 53; // error
}
method NoChangeAndCorrect()
{
assert true;
}
|