View source for Proof Obligation Names (Rodin User Manual)

{| class="wikitable" style="font-style:italic; text-align: center; font-size:120%; border: 3px dashed red;"
|-
! scope="col" | Do not edit!  This content has been migrated to Subversion.
|-
|([http://handbook.event-b.org Nightly Handbook Build])
|}

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-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
|}
</center>

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

<center>
{{SimpleHeader}}
|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 
|}
</center>

Next are the proof obligations concerned with machine refinements:
<center>
{{SimpleHeader}}
|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 
|}
</center>


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

<center>
{{SimpleHeader}}
|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
|}
</center>
Finally, here are the proof obligations concerned with witnesses:

<center>
{{SimpleHeader}}
|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
|}
</center>

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.


[[Category:User documentation|Proof Obligation Names]]
[[Category:Rodin Platform|Proof Obligation Names]]
[[Category:User manual|Proof Obligation Names]]
[[Category:Proof]]