Isabelle/UTP

A verification toolbox for Isabelle/HOL based on Unifying Theories of Programming

View project on GitHub

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 also trop, 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 to var, but by convention used to refer to a predicate variable.
  • $x : (\(\tau, \alpha \times \beta\) uexpr) for x : \(\tau \Longrightarrow \alpha\) – a relational input variable.
  • $y' : (\(\tau, \alpha \times \beta\) uexpr) for y : \(\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