Isabelle/UTP

UTP Variables

Variables in Isabelle/UTP are modelled using lenses, rather than as explicitly named entities. It is therefore crucial to understand the basics of lenses in order to correctly model program state in Isabelle/UTP. A lens \(x : V \Longrightarrow S\) shows how a given type \(V\) can be viewed from “larger” source type \(S\), as illustrated below (the hatched region of the source corresponds to the view).

Lenses thus allow us to treat variables as different observations of the state-space of a predicate. Importantly, they are characterised semantically, rather than syntactically, using the put and get functions. Thus, meta-logical properties of variables, such as whether a program fragment depends on a variable, can be characterised as algebraic properties of these two functions. As is typical, we restrict lenses to the class of very well-behaved lenses, so that get and put are tied together in an appropriate way. In Isabelle/UTP laws that use lenses often have the proviso vwb_lens x, for example.

We define the following core properties of lenses:

• Independence: \(x \bowtie y\), states that x and y observe disjoint regions of a common state-space.
• Sublens: \(x \subseteq_L y\), states that the view of x is within the view of y.
• Equivalence: \(x \approx_L y\), states that two lenses observe equivalent regions.

For example, independence can be used to state that two variables are different, which is useful in stating many laws of programming in UTP. More importantly, it allows us to semantically characterise state-space separation which is very important when modelling concurrency (cf. separation logic). These functions can be used to compare lenses with different view types; they must only share the same view type. We also define various basic lenses and lens combinators.

• Zero lens: \(0_L : () \Longrightarrow S\), a lens whose view is the unit type () and thus cannot distinguish any state-spaces. It is the smallest lens ordered by sublens.
• One lens: \(0_L : S \Longrightarrow S\), a lens whose view is the same as the source and thus is maximally distinguishing of the source type. It is therefore the largest lens ordered by sublens.
• Composition: \(x \,;_L\, y\) for \(x : V_1 \Longrightarrow V_2\) and \(y : V_2 \Longrightarrow S\) constructs a “longer” lens that identifies the source type of x with the view type of y.
• Summation: \(x \,+_L\, y : V_1 \times V_2 \Longrightarrow S\) for \(x : V_1 \Longrightarrow S\) and \(y : V_2 \Longrightarrow S\), observes the view types of x and y simultaneously.

The one lens can be used to refer to the entire state-space of a program. The sum lens can be used to collect variables in sets, to semantically characterise multiple variables. For example, assuming that x, y, and z are independent lenses, then the characteristic set {x, y, z} can be expressed as \((x \,+_L\, y \,+_L\, z)\), that is the lens that views all three lenses’ regions simultaneously.

These operators also have an associated set of intuitive algebraic laws, for example \(0_L \,+_L\, X ~\approx_L~ X\) (which also hints at why it is important that equivalence is heterogeneously types). For more information, please see our ICTAC paper.