Proof Obligations Sample Clauses

Proof Obligations. For a combination of a flow and machine we would like to be able to demonstrate that the flow is consistent or concrete (the latter requires the former). The general strategy is split an overall proof into a collection of simpler conditions. For flow consistency, a suitable way to do this is to analyse each instance of sequential composition individually as suggested by the condition of Theorem 1 (see Definition 6 for oper- ator cons). For an instance of a sequential composition, from Definition 5 we have the following feasibility condition for a composed event. I(v) G(p, v) vj (S(p, v, vj); ( q H(q, v) R(q, v, vj))) v1 (S(p, v, v1) q H(q, v1) R(q, v1, vj))) The condition is far too complex in the current form. A more compact one could be found. Let us first assume that the composed events are feasible on their own. This gives the following two axioms. axm1 : I(v) G(p, v) vj S(p, v, vj) axm2 : I(v) H(q, v) vj R(q, v, vj) Applying axiom axm1, the feasibility condition for a composed event is simplified to the following: I(v) ∧ G(p, v) ∧ S(p, v, v1) € ∃ q · H(q, v1) ∧ R(q, v1, vj) With the help of the second axiom we are able to remove R(q, v1, vj) clause from the goal: I(v) ∧ G(p, v) ∧ S(p, v, v1) € ∃ q · H(q, v1) Finally, extending the above with the consideration of model constants and sets, the follow- ing proof obligation is formulated. P(c, s) ∧ I(c, s, v) ∧ G(c, s, pe, v) ∧ S(c, s, pe, v, vj) € H(c, s, q, v) Here G and S are the guard and before-after predicate (actions) of what is possibly a result of merging several model events. The proof obligation demonstrates that an event characterised by G and S is able to pass control to another (possibly merged) event with guard H for any possible state permitted by G. The axioms we have rely upon are sound since they are a part of model consistency proof obligations that are to be discharge for every Event-B model[3]. With a similar procedure we are able to find a practical form of a proof obligation for demon- strating that a flow is concrete. The following proof obligation requires that for a given instance p; q of a sequential composition the choice branches in q, if there any, are mutually exclusive. . j j(H (c s q v ) H (c s q v )) P(c, s) ∧ I(c, s, v) ∧ G(c, s, p, v) ∧ S(c, s, p, v, vj) € {s,t}∈EN(q)∧sƒ=t ¬ s , , s, ∧ t , , t , Here Hs and Ht are the guards of possibly merged events. The goal in this proof obligation may become lengthy in some extreme case when there is a choice on a large number of e...