Rodin HandbookThis work is sponsored by the Deploy Project This work is sponsored by the ADVANCE Project This work is licensed under a Creative Commons Attribution 3.0 Unported License |
3.2.5 Well-definedness proof obligationsThere are several locations where well-definedness proof obligations can be created. The mathematical notation of the well-definedness conditions of each operator are defined by the -operator (3.3.1.2). For well-definedness conditions, the order of axioms, invariants and guards is important. Well-definedness conditions are not usually shown in Rodin if they are trivial (). 3.2.5.1 AxiomsFor an axiom , denotes (the conjunction of) all axioms declared in extended contexts and the axioms already declared in the current context before the axiom in question.
3.2.5.2 InvariantsFor an invariant , denotes (the conjunction of) all the model’s invariants declared before the theorem.
3.2.5.3 GuardsFor an invariant , denotes (the conjunction of) all the model’s invariants declared before the theorem.
3.2.5.4 WitnessesA witness may contain well-definedness conditions.
3.2.5.5 ActionsThe assignment of each action with the label in an event must be well-defined.
3.2.5.6 VariantsA variant must be well-defined.
|