equal
deleted
inserted
replaced
9 *) |
9 *) |
10 |
10 |
11 SubstAx = WFair + Constrains + |
11 SubstAx = WFair + Constrains + |
12 |
12 |
13 constdefs |
13 constdefs |
|
14 (* The definitions below are not `conventional', but yields simpler rules *) |
14 Ensures :: "[i,i] => i" (infixl 60) |
15 Ensures :: "[i,i] => i" (infixl 60) |
15 "A Ensures B == {F:program. F : (reachable(F) Int A) ensures B & |
16 "A Ensures B == {F:program. F : (reachable(F) Int A) ensures (reachable(F) Int B) }" |
16 A:condition & B:condition}" |
|
17 |
17 |
18 LeadsTo :: "[i, i] => i" (infixl 60) |
18 LeadsTo :: "[i, i] => i" (infixl 60) |
19 "A LeadsTo B == {F:program. F:(reachable(F) Int A) leadsTo B & |
19 "A LeadsTo B == {F:program. F:(reachable(F) Int A) leadsTo (reachable(F) Int B)}" |
20 A:condition & B:condition}" |
|
21 |
20 |
22 syntax (xsymbols) |
21 syntax (xsymbols) |
23 "op LeadsTo" :: "[i, i] => i" (infixl " \\<longmapsto>w " 60) |
22 "op LeadsTo" :: "[i, i] => i" (infixl " \\<longmapsto>w " 60) |
24 |
23 |
25 end |
24 end |