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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
// this test is for the automatic trigger generation
class Triggers
{
var next : Triggers // to allow recursive definitions
predicate valid { acc(next) && next != null && next.valid } // intentionally doesn't terminate - allows function definitions to be unknown
function f(x,y,z : int):bool
requires valid
{
unfolding valid in next.f(x,y,z) // unknown definition
}
function h(x,y,z : int):bool
requires valid
{
unfolding valid in next.h(x,y,z) // unknown definition
}
function g(x : int) : bool
requires valid
{
unfolding valid in next.g(x) // unknown definition
}
function i(x:int, y:bool) : bool
requires valid
{
unfolding valid in next.i(x,y) // unknown definition
}
method triggers_one()
requires valid
requires (forall a : int :: !(g(a) ==> false))
ensures valid
ensures (forall b : int :: g(b))
{ }
method triggers_two()
requires valid
requires (forall a,b,c : int :: ( g(a) && f(a,b,c)))
ensures valid
ensures (forall x,y,z : int :: f(x,y,z))
ensures (forall w : int :: (g(w))) // fails because there isn't a good enough trigger for finding g(w)
{ }
method triggers_three()
requires valid
requires (forall a : int :: ( g(a) && (forall b,c : int :: f(a,b,c))))
ensures valid
ensures (forall x,y,z : int :: f(x,y,z)) // fails because of the trigger chosen for a (g(a)).
ensures (forall w : int :: (g(w)))
{ }
method triggers_four()
requires valid
requires (forall a,b,c,d,e:int :: f(a,b,c) && h(b,c,d) && f(c,d,e))
ensures valid
ensures (forall x,y,z : int :: f(x,y,z)) // fails - not enough triggers
ensures (forall x,y,z : int :: f(x,y,z) && f(z,y,x)) // succeeds - {f(a,b,c),f(c,d,e)} is one of the trigger sets which should be found
{ }
method triggers_five(c : bool, d : bool)
requires c ==> d
requires valid
requires (forall x : int :: i(x, (c ==> d))) // check that logical operators are suitably avoided in triggers
ensures valid
ensures i(4,true)
{ }
method triggers_six(c : int, d : int)
requires c > d
requires valid
requires (forall x : int :: i(x, (c > d))) // check that logical operators are suitably avoided in triggers
ensures valid
ensures i(4,true)
{ }
}
|
