Alphabetised Relational Calculus
The core of the UTP is the alphabetised relational calculus which acts as a lingua franca for denotational semantics
of programming and modelling languages. The relational calculus combines typical predicate calculus operators, such as
Boolean connectives, with binary relation algebra operators such as sequential composition and if-then-else
conditional. The main type for relations is \((\alpha,\beta)\) rel
, where \(\alpha\) and \(\beta\) are the input
and output alphabet types, respectively. This is synonymous with the alphabetised predicate \((\alpha \times \beta)\)
upred
, that is the alphabet is a produce type. There is also \(\alpha\) hrel
when a homogeneous relation is
required. Conditions can be expressed using predicate operators.
The main operators of the mechansied relational calculus and their types are give below.
- Sequential composition:
P ;; Q
, forP :: \((\alpha,\beta)\) rel
andQ :: \((\beta,\gamma)\) rel
- Conditional (infix if-then-else):
P \(\infixIf\) b \(\infixElse_r\) Q
, forP, Q :: \((\alpha,\beta)\) rel
andb :: \(\alpha\) upred
- Assignment:
\(\langle \sigma \rangle_a\) :: \(\alpha\) hrel
, for\(\sigma\) :: \(\alpha \Rightarrow \alpha\)
- Identity (skip):
II :: \(\alpha\) hrel
- Universal relation:
true :: \((\alpha,\beta)\) rel
- Empty relation:
false :: \((\alpha,\beta)\) rel
- Weakest fixed-point:
\(\mu X \bullet F(X)\)
, forF :: \((\alpha,\beta)\) rel \(\Rightarrow\) \((\alpha,\beta)\) rel
The assignment operator is inspired the one from Back’s refinement calculus. It takes a function \(\sigma\) which
corresponds to a state update or substitution, in that it maps an old state to a new one. A single
variable assignment can also be written x := v
, where x
is a lens \(\tau \Longrightarrow \alpha\)
, that is a
variable in state-space \(\alpha\) whose type is \(\tau\), and v
is an expression \((\tau, \alpha)\) uexpr
. This
operator corresponds to \(\langle [x \mapsto_s v]\rangle_a\)
.
For relations, we also employ a number of alphabet extrusions. The syntax \(\lceil P \rceil_<\)
for \(P : \alpha\)
upred
is used to a lift a condition on initial variables to a relation of type \((\alpha, \beta)\) rel
. It
corresponds to the alphabet extrusion \(P \oplus_p \textit{fst}_L\)
, where \(\textit{fst}_L : \alpha \Longrightarrow
\alpha \times \beta\) is the lens that projects the first element of a produce state space. Similarly, we have the
syntax \(\lceil Q \rceil_>\)
for \(Q : \beta\) upred
that constructs a postcondition relation of type \((\alpha,
\beta)\) rel
using the \(\textit{snd}_L\) lens.
Isabelle/UTP is supported by projects INTO-CPS, RoboCalc, and CyPhyAssure