blob: 6a2d9640eacc09266ef3220cd79e6121ce3c928f (
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
|
// RUN: %boogie "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// inlined functions
function Twice(x: int) returns (int)
{
x + x
}
function {:inline} Double(x: int) returns (int)
{
3 * x - x
}
function f(int) returns (int);
function g(int) returns (int);
function h(int) returns (int);
function k(int) returns (int);
axiom (forall x: int :: Twice(x) == f(x)); // here, Twice(x) and f(x) are both triggers
axiom (forall x: int :: Double(x) == g(x)); // since Double is inlined, the trigger here is just g(x)
axiom (forall x: int :: { f(x) } f(x) < h(x) );
axiom (forall x: int :: { g(x) } g(x) < k(x) );
procedure P(a: int, b: int, c: int)
{
// The following is provable, because Twice triggers its definition and the resulting f(a)
// triggers the relation to h(a).
assert Twice(a) < h(a);
if (*) {
// The following is NOT provable, because Double is inlined and thus no g(b) term is ever
// created
assert Double(b) < k(b); // error
} else {
// The following IS provable, because the explicit g(c) will cause both of the necessary
// quantifiers to trigger
assert g(c) == 2*c;
assert Double(c) < k(c);
}
}
// nullary functions
function Five() returns (int) { 5 }
function {:inline} Eight() returns (e: int) { 8 }
procedure Q()
{
assert 8 * Five() == 5 * Eight();
}
|