Rodin User’s Handbook v.2.8: Well-definedness proof obligations

3.2.5 Well-definedness proof obligations

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 $\mathcal{L}$ -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 ( $\mathord {\top }$ ).

3.2.5.1 Axioms

For an axiom $A_ w$ , $A_ b$ 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	$A_ b \mathbin \Rightarrow \mathcal{L}(A_ w)$

3.2.5.2 Invariants

For an invariant $J_ w$ , $J_ b$ denotes (the conjunction of) all the model’s invariants declared before the theorem.

	Well-definedness of an invariant
Name	label/WD
Goal	$A \land I \land J_ b \mathbin \Rightarrow \mathcal{L}(J_ w)$

3.2.5.3 Guards

For an invariant $H_ w$ , $H_ b$ denotes (the conjunction of) all the model’s invariants declared before the theorem.

	Well-definedness of a guard
Name	eventname/guardlabel/WD
Goal	$A \land I \land J \land H_ b \mathbin \Rightarrow \mathcal{L}(H_ w)$

3.2.5.4 Witnesses

A witness $W$ may contain well-definedness conditions.

	Well-definedness of a witness
Name	eventlabel/witnesslabel/WWD
Goal	$A \land I \land J \land \mathcal{T}\mathbin \Rightarrow \mathcal{L}(W)$

3.2.5.5 Actions

The assignment $a$ of each action with the label $\textsf{actionlabel}$ in an event must be well-defined.

	Well-definedness of an action
Name	eventlabel/actionlabel/WD
Goal	$A \land I \land J \land G \land H \mathbin \Rightarrow \mathcal{L}(~ a~ )$

3.2.5.6 Variants

A variant $V$ must be well-defined.

	Well-definedness of a variant
Name	VWD
Goal	$A \land J \mathbin \Rightarrow \mathcal{L}(V)$

Rodin Handbook