There 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 ().
For 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.
Well-definedness of an axiom |
|
Name |
label/WD |
Goal |
|
.
For an invariant ,
denotes (the conjunction of) all the model’s invariants declared before the theorem.
Well-definedness of an invariant |
|
Name |
label/WD |
Goal |
|
For an invariant ,
denotes (the conjunction of) all the model’s invariants declared before the theorem.
Well-definedness of a guard |
|
Name |
eventname/guardlabel/WD |
Goal |
|
A witness may contain well-definedness conditions.
Well-definedness of a witness |
|
Name |
eventlabel/witnesslabel/WWD |
Goal |
|
The assignment of each action with the label
in an event must be well-defined.
Well-definedness of an action |
|
Name |
eventlabel/actionlabel/WD |
Goal |
|
A variant must be well-defined.
Well-definedness of a variant |
|
Name |
VWD |
Goal |
|