# Proof Obligation Names (Rodin User Manual)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
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 [itex]m[/itex] / WD [itex]m[/itex] is the axiom name Well-definedness of a Derived Axiom [itex]m[/itex] / WD [itex]m[/itex] is the axiom name Derived Axiom [itex]m[/itex] / THM [itex]m[/itex] is the axiom name

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

 Well-definedness of an Invariant [itex]v[/itex] / WD [itex]v[/itex] is the invariant name Well-definedness of a Derived Invariant [itex]m[/itex] / WD [itex]m[/itex] is the invariant name Well-definedness of an event Guard [itex]t[/itex] / [itex]d[/itex] / WD [itex]t[/itex] is the event name [itex]d[/itex] is the action name Well-definedness of an event Action [itex]t[/itex] / [itex]d[/itex] / WD [itex]t[/itex] is the event name [itex]d[/itex] is the action name Feasibility of a non-det. event Action [itex]t[/itex] / [itex]d[/itex] / FIS [itex]t[/itex] is the event name [itex]d[/itex] is the action name Derived Invariant [itex]m[/itex] / THM [itex]m[/itex] is the invariant name Invariant Establishment INIT. / [itex]v[/itex] / INV [itex]v[/itex] is the invariant name Invariant Preservation [itex]t[/itex] / [itex]v[/itex] / INV [itex]t[/itex] is the event name [itex]v[/itex] is the invariant name

Next are the proof obligations concerned with machine refinements:

 Guard Strengthening [itex]t[/itex] / [itex]d[/itex] / GRD [itex]t[/itex] is the concrete event name [itex]d[/itex] is the abstract guard name Guard Strengthening (merge) [itex]t[/itex] / MRG [itex]t[/itex] is the concrete event name Action Simulation [itex]t[/itex] / [itex]d[/itex] / SIM [itex]t[/itex] is the concrete event name [itex]d[/itex] is the abstract action name Equality of a preserved Variable [itex]t[/itex] / [itex]v[/itex] / EQL [itex]t[/itex] is the concrete event name [itex]v[/itex] 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 [itex]t[/itex] / NAT [itex]t[/itex] is the new event name Decreasing of Variant [itex]t[/itex] / VAR [itex]t[/itex] is the new event name

Finally, here are the proof obligations concerned with witnesses:

 Well definedness of Witness [itex]t[/itex] / [itex]p[/itex] / WWD [itex]t[/itex] is the concrete event name [itex]p[/itex] is parameter name or a primed variable name Feasibility of non-det. Witness [itex]t[/itex] / [itex]p[/itex] / WFIS [itex]t[/itex] is the concrete event name [itex]p[/itex] 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.