# 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 | / WD | is the axiom name |

Well-definedness of a Derived Axiom | / WD | is the axiom name |

Derived Axiom | / THM | is the axiom name |

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

Well-definedness of an Invariant | / WD | is the invariant name |

Well-definedness of a Derived Invariant | / WD | is the invariant name |

Well-definedness of an event Guard | / / WD | is the event name
is the action name |

Well-definedness of an event Action | / / WD | is the event name
is the action name |

Feasibility of a non-det. event Action | / / FIS | is the event name
is the action name |

Derived Invariant | / THM | is the invariant name |

Invariant Establishment | INIT. / / INV | is the invariant name |

Invariant Preservation | / / INV | is the event name
is the invariant name |

Next are the proof obligations concerned with machine refinements:

Guard Strengthening | / / GRD | is the concrete event name
is the abstract guard name |

Guard Strengthening (merge) | / MRG | is the concrete event name |

Action Simulation | / / SIM | is the concrete event name
is the abstract action name |

Equality of a preserved Variable | / / EQL | is the concrete event name
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 | / NAT | is the new event name |

Decreasing of Variant | / VAR | is the new event name |

Finally, here are the proof obligations concerned with witnesses:

Well definedness of Witness | / / WWD | is the concrete event name
is parameter name or a primed variable name |

Feasibility of non-det. Witness | / / WFIS | is the concrete event name
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.