equal
deleted
inserted
replaced
19 (*F's program*) |
19 (*F's program*) |
20 cmdF :: "(state*state) set" |
20 cmdF :: "(state*state) set" |
21 "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}" |
21 "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}" |
22 |
22 |
23 F :: "state program" |
23 F :: "state program" |
24 "F == mk_program (UNIV, {s. NF s = 0 & BB s}, {cmdF})" |
24 "F == mk_program ({s. NF s = 0 & BB s}, {cmdF})" |
25 |
25 |
26 (*G's program*) |
26 (*G's program*) |
27 cmdG :: "(state*state) set" |
27 cmdG :: "(state*state) set" |
28 "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}" |
28 "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}" |
29 |
29 |
30 G :: "state program" |
30 G :: "state program" |
31 "G == mk_program (UNIV, {s. NG s = 0 & BB s}, {cmdG})" |
31 "G == mk_program ({s. NG s = 0 & BB s}, {cmdG})" |
32 |
32 |
33 (*the joint invariant*) |
33 (*the joint invariant*) |
34 invFG :: "state set" |
34 invFG :: "state set" |
35 "invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}" |
35 "invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}" |
36 |
36 |