3.2.4 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.4.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(\mathbf{c}) \mathbin \Rightarrow \mathcal{L}(A_ w(\mathbf{c}))$

.

3.2.4.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(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J_ b(\mathbf{c},\mathbf{v},\mathbf{w}) \mathbin \Rightarrow \mathcal{L}(J_ w(\mathbf{c},\mathbf{v},\mathbf{w}))$

3.2.4.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(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land H_ b(\mathbf{c},\mathbf{w},\mathbf{u}) \mathbin \Rightarrow \mathcal{L}(H_ w(\mathbf{c},\mathbf{w},\mathbf{u}))$

3.2.4.4 Witnesses

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

 

Well-definedness of a witness

Name

eventlabel/witnesslabel/WWD

Goal

$A(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land \mathcal{T}(\mathbf{c},\mathbf{u},\mathbf{w},\mathbf{w}’)\mathbin \Rightarrow \mathcal{L}(W)$

3.2.4.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(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land G(\mathbf{c},\mathbf{v},\mathbf{t})\land H(\mathbf{c},\mathbf{w},\mathbf{u})\mathbin \Rightarrow \mathcal{L}(~ a~ )$

3.2.4.6 Variants

A variant $V(\mathbf{c},\mathbf{w})$ must be well-defined.

 

Well-definedness of a variant

Name

VWD

Goal

$A(\mathbf{c})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\mathbin \Rightarrow \mathcal{L}(V(\mathbf{c},\mathbf{w}))$