# Proof Obligation Names (Rodin User Manual)

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.