Isabelle/UTP

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, for P :: \((\alpha,\beta)\) rel and Q :: \((\beta,\gamma)\) rel
• Conditional (infix if-then-else): P \(\infixIf\) b \(\infixElse_r\) Q, for P, Q :: \((\alpha,\beta)\) rel and b :: \(\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)\), for F :: \((\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.