Proof Obligation Names (Rodin User Manual)

From Event-B

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.