UTP Expressions
Expressions form the core of the UTP program model: everything is built on top of them. They are characterised by the
Isabelle/HOL type \((\tau, \alpha)\) uexpr
. Here, \(\tau\) is the return type of the expression and \(\alpha\) is
the state-space type or alphabet. In UTP, the alphabet the denotes the possible variables that a predicate is permitted
to refer to. Attempting to write a predicate using variables outside its alphabet is a type error, and this is reflected
in Isabelle/UTP where variables must be lenses whose source is the alphabet.
The following core functions allow us to construct expressions.
- Literals:
«v»
– lift HOL value\(v : \tau\)
to a UTP expression of type\((\tau, \alpha)\) uexpr
- Unary Operators:
uop : \((a \Rightarrow b) \Rightarrow\) \((a, \alpha)\) uexpr \(\Rightarrow\) \((b, \alpha)\) uexpr
– lifts a unary HOL function to an expression operator - Binary Operators:
bop
– lifts a binary HOL function (see alsotrop
,qtop
)
Additionally, built-in HOL syntax, like numerals and arithmetic operators, are supported by the expression model. We also lift a operators on partial functions, sets, and other data structures, though sometimes renamings are required to the operators. For details of built-in operators, please see the syntax reference guide.
For variables, the key construct is var : \((\tau \Longrightarrow \alpha)\) \(\Rightarrow\) \((\tau, \alpha)\) uexpr
which lifts a lens to an expression which returns the corresponding view type. Usually var
is not used directly, but
one of the syntactic constructions below.
&x
– essentially identical tovar
, but by convention used to refer to a predicate variable.$x : (\(\tau, \alpha \times \beta\) uexpr)
forx : \(\tau \Longrightarrow \alpha\)
– a relational input variable.$y' : (\(\tau, \alpha \times \beta\) uexpr)
fory : \(\tau \Longrightarrow \beta\)
– a relational output variable.
In mathematical UTP (i.e. the UTP used by Hoare, He, Woodcock, Cavalcanti and others), it is not necessary to distinguish
&x
and $x
, but here it is because they have different source types. The relational variables lift a lens to one that
views the first or second element of a product type, repectively for inputs and outputs. We will consider this more in
the section on relations.
An expression with a boolean return type is called a predicate. The type \(\alpha\) upred \(\triangleq\) \((bool,
\alpha)\) uexpr
, for alphabet type \(\alpha\), is the core type of the alphabetised predicate calculus. We use the
expression operators above to lift the typical predicate operators of HOL, like \(\wedge\) and \(\exists\), to
operators of the UTP predicate calculus.
Isabelle/UTP is supported by projects INTO-CPS, RoboCalc, and CyPhyAssure