Proof Obligation Names (Rodin User Manual)

From Event-B
Revision as of 16:09, 15 September 2011 by Ladenberger (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, 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 <math>m</math> / WD <math>m</math> is the axiom name
Well-definedness of a Derived Axiom <math>m</math> / WD <math>m</math> is the axiom name
Derived Axiom <math>m</math> / THM <math>m</math> is the axiom name

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

Well-definedness of an Invariant <math>v</math> / WD <math>v</math> is the invariant name
Well-definedness of a Derived Invariant <math>m</math> / WD <math>m</math> is the invariant name
Well-definedness of an event Guard <math>t</math> / <math>d</math> / WD <math>t</math> is the event name

<math>d</math> is the action name

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

<math>d</math> is the action name

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

<math>d</math> is the action name

Derived Invariant <math>m</math> / THM <math>m</math> is the invariant name
Invariant Establishment INIT. / <math>v</math> / INV <math>v</math> is the invariant name
Invariant Preservation <math>t</math> / <math>v</math> / INV <math>t</math> is the event name

<math>v</math> is the invariant name

Next are the proof obligations concerned with machine refinements:

Guard Strengthening <math>t</math> / <math>d</math> / GRD <math>t</math> is the concrete event name

<math>d</math> is the abstract guard name

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

<math>d</math> is the abstract action name

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

<math>v</math> 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 <math>t</math> / NAT <math>t</math> is the new event name
Decreasing of Variant <math>t</math> / VAR <math>t</math> is the new event name

Finally, here are the proof obligations concerned with witnesses:

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

<math>p</math> is parameter name

or a primed variable name

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

<math>p</math> 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.