blob: c163ed181f73998b0d40b96b58a12f484eb1698e (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
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;
}
|