blob: fc14a0eb41fde1a16583db5334fdb5ccd5bd8350 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
function xxgz(x:int) returns(bool);
function xxf1(x:int,y:bool) returns(int);
axiom {:inline true} (forall x:int :: xxgz(x) <==> x > 0);
axiom {:inline true} (forall x:int, y:bool :: xxf1(x,y) == x+1);
axiom (forall z:int :: z>12 ==> xxgz(z));
axiom (forall y:int, x:bool :: xxf1(y, x) > 1 ==> y > 0);
procedure foo()
{
assert xxgz(12);
assert xxf1(3,true) == 4;
}
|
