equal
deleted
inserted
replaced
29 Init "s: Init F ==> s : reachable F" |
29 Init "s: Init F ==> s : reachable F" |
30 |
30 |
31 Acts "[| act: Acts F; s : reachable F; (s,s'): act |] |
31 Acts "[| act: Acts F; s : reachable F; (s,s'): act |] |
32 ==> s' : reachable F" |
32 ==> s' : reachable F" |
33 |
33 |
|
34 consts |
|
35 Co, Unless :: "['a set, 'a set] => 'a program set" (infixl 60) |
|
36 |
|
37 defs |
|
38 Constrains_def |
|
39 "A Co B == {F. F : (reachable F Int A) co (reachable F Int B)}" |
|
40 |
|
41 Unless_def |
|
42 "A Unless B == (A-B) Co (A Un B)" |
|
43 |
34 constdefs |
44 constdefs |
35 |
45 |
36 Constrains :: "['a set, 'a set] => 'a program set" |
|
37 "Constrains A B == {F. F : constrains (reachable F Int A) |
|
38 (reachable F Int B)}" |
|
39 |
|
40 Stable :: "'a set => 'a program set" |
46 Stable :: "'a set => 'a program set" |
41 "Stable A == Constrains A A" |
47 "Stable A == A Co A" |
42 |
|
43 Unless :: "['a set, 'a set] => 'a program set" |
|
44 "Unless A B == Constrains (A-B) (A Un B)" |
|
45 |
48 |
46 Invariant :: "'a set => 'a program set" |
49 Invariant :: "'a set => 'a program set" |
47 "Invariant A == {F. Init F <= A} Int Stable A" |
50 "Invariant A == {F. Init F <= A} Int Stable A" |
48 |
51 |
49 (*Polymorphic in both states and the meaning of <= *) |
52 (*Polymorphic in both states and the meaning of <= *) |