blob: 4052601166c6ee82a3c88802b9b435987352fd4e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
type ref;
function choose(a:bool, b:int, c:int) returns (x:int);
axiom(forall a:bool, b:int, c:int :: {choose(a,b,c)} a ==> choose(a,b,c) == b);
var myInt:int;
procedure main()
modifies myInt;
ensures myInt==5;
{
myInt:=4;
}
|