Proof Obligation Names (Rodin User Manual)

From Event-B
Revision as of 09:57, 28 February 2009 by imported>Mathieu (New page: Next is a table describing the names of context proof obligations: <center> {{SimpleHeader}} |Well-definedness of an Axiom||<math>m</math> / WD||<math>m</math> is the axiom name |- |Well...)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

Next is a table describing the names of context proof obligations:

Well-definedness of an Axiom m / WD m is the axiom name
Well-definedness of a Theorem m / WD m is the theorem name
Theorem m / THM m is the theorem name

Next is a table showing the name of machine proof obligations:

Well-definedness of an Invariant v / WD v is the invariant name
Well-definedness of a Theorem m / WD m is the theorem name
Well-definedness of an event Guard t / d / WD t is the event name

d is the action name

Well-definedness of an event Action t / d / WD t is the event name

d is the action name

Feasibility of a non-det. event Action t / d / FIS t is the event name

d is the action name

Theorem m / THM m is the theorem name
Invariant Establishment INIT. / v / INV v is the invariant name
Invariant Preservation t / v / INV t is the event name

v is the invariant name

Next are the proof obligations concerned with machine refinements:

Guard Strengthening t / d / GRD t is the concrete event name

d is the abstract guard name

Guard Strengthening (merge) t / MRG t is the concrete event name
Action Simulation t / d / SIM t is the concrete event name

d is the abstract action name

Equality of a preserved Variable t / v / EQL t is the concrete event name

v is the preserved variable


Next are the proof obligations concerned with the new events variant:

Well definedness of Variant VWD
Finiteness for a set Variant FIN
Natural number for a numeric Variant t / NAT t is the new event name
Decreasing of Variant t / VAR t is the new event name

Finally, here are the proof obligations concerned with witnesses:

Well definedness of Witness t / p / WWD t is the concrete event name

p is parameter name

or a primed variable name

Feasibility of non-det. Witness t / p / WFIS t is the concrete event name

p is parameter name

or a primed variable name

Remark: At the moment, the deadlock freeness proof obligation generation is missing. If you need it, you can generate it yourself as a theorem saying the the disjunction of the abstract guards imply the disjunction of the concrete guards.