Proof Obligation Names (Rodin User Manual)

From Event-B
Jump to navigationJump to search
Do not edit! This content has been migrated to Subversion.
(Nightly Handbook Build)

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 Derived Axiom m / WD m is the axiom name
Derived Axiom m / THM m is the axiom 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 Derived Invariant m / WD m is the invariant 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

Derived Invariant m / THM m is the invariant 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 derived invariant saying the the disjunction of the abstract guards imply the disjunction of the concrete guards.