Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP

The growing complexity and diversity of models used in the engineering of dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and presentations, must be integrated. Such an integration relies on unified semantic foundations for the various notations, and co-ordination of a variety of automated verification tools. The contribution of this paper is Isabelle/UTP, an implementation of Hoare and He's Unifying Theories of Programming, a framework for unification of formal semantics. Isabelle/UTP permits the mechanisation of computational theories for diverse paradigms, and their use in constructing formalised semantic models. These can be further applied in the development of verification tools, harnessing Isabelle/HOL's powerful proof automation facilities. Several layers of mathematical foundations are developed, including lenses to model variables and state spaces as algebraic objects, alphabetised predicates and relations to model programs, including algebraic and axiomatic semantics, and UTP theories to encode computational paradigms. We illustrate our approach with a variety of proof tools, and in particular develop a verification tool for the formal state machine notation, RoboChart.


Introduction
Unifying Theories of Programming [43] (UTP) is a framework for capturing, unifying, and integrating formal semantics of programming languages using predicate and relational calculus. It aims to provide a coherent structure for the intellectual discipline of computer science, by characterising the various programming languages it has produced, their foundational computational paradigms, and the various approaches to presentation of formal semantics [43]. In one axis, UTP allows us to study the plethora of computational paradigms -such as functional, imperative, concurrent [43,55], real-time [62], and hybrid dynamical systems [28,27] -using "UTP theories": semantic components that allow us to construct heterogeneous semantic models. In another axis, it allows us to characterise and link different presentations of semantics, such as axiomatic semantics, like Hoare logic, refinement calculus, and separation logic, with operational semantics, such as big-step and small-step, and also algebraic semantics.
The UTP employs Hehner's "programs-as-predicates" approach [36,38], where a program is modelled as a relational predicate over initial and final, or intermediate, observations of the state. The observation space may consist of both the internal state of a computer, such as its program variables and objects, and also modelled quantities of the real-world, such as time and physical interactions. The UTP approach provides a universal domain for both deterministic programs and non-deterministic specifications. These can be formally related through refinement, S P, which states that P is refined by S, and corresponds to universally closed implication. Moreover, the embedding of programs into logic means that formal verification, using the afformentioned axiomatic calculi, can be aided by automated theorem provers and SMT solvers.
Though the original emphasis of UTP is on programming languages, it can also be used to provide semantics for high-level modelling languages and diagrammatic notations. The use of UTP, crucially, enables us to provide various semantic models that account for different computational paradigms, and yet are linked through a common foundation. With adequate tool support, UTP can therefore allow us to answer  [9], and other paradigms [28]. Our work therefore also serves as a template for building automated verification tools with Isabelle/UTP. In §2 we describe background materials for our work. Following this, in sections 3 to 7, we give an exposition of our contributions. The paper overview given in Figure 2 shows how the various foundational parts of Isabelle/UTP are connected, and the sections in which they are documented. In §3 we describe how state spaces and variables in a program can be modelled algebraically using lenses. In §4 we describe the core of Isabelle/UTP, first defining its expression model in §4.1, predicates in §4.2, and the relational program model in §4.6 with proof support and mechanised laws of programming. In §5 we utilise this relational program model, to build tools for symbolic evaluation and verification using Hoare calculus. In §6 we describe how different computational paradigms can be captured and mechanised using Isabelle/UTP theories, and illustrate this using a UTP theory for concurrent and reactive programs. In §7 we use our UTP theory of reactive programs to build a verification tool for state machines. Finally in §8, we conclude. This paper is an extension of two conference papers [33,25]. We extend and refine the material on modelling state spaces using lenses from [33], and give a fuller account of their use in the foundations of Isabelle/UTP. We extend [25] with further materials on how UTP theories are mechanised, building on the results given in [33]. We stress that all the definitions, theorems, and proofs in this paper are mechanically validated in Isabelle/HOL. On the whole, we simply present the core theorems without proofs, and therefore refer the interested reader to a number of companion reports [30,31]. Though our work is primarily based on Isabelle/HOL, we prefer to use more traditional mathematical notations [63,43] in this work, since we believe this makes the results more accessible.

Background and Related Work
In this section we review some preliminary material, and highlight related work.

Unifying Theories of Programming
The last decade of the twentieth century saw several seminal works on integrating formal methods in order to allow their insertion into the software engineering lifecycle [10] across its diverse notations [56,34]. These works emphasise the centrality of unified formal semantics [38,37] for the various models and artefacts. An important development in this direction is Hoare and He's Unifying Theories of Programming [42,43,16] (UTP), which draws together results from several intellectual streams, notably Hehner's predicative programming [36,38], Tarski's relational calculus [64], Dijkstra's guarded command language [17], and the refinement calculi of Back [3] and Morgan [50].
UTP supports formalisation of computational semantic domains that are used to give denotational semantics to a variety of programming and modelling languages. It employs alphabetised binary relations to model programs as predicates [36,37] relating the initial values of variables (x) to their later values (x ). UTP divides variables into two classes: (1) program variables, that model data, and (2) observational variables, that encode additional semantic structure. For example, clock : N is a variable to record the passage of time. Unlike a program variable, it makes no sense to assign values to clock, as this would model arbitrary time travel. Therefore, observational variables are constrained using healthiness conditions, which are encoded as idempotent functions on predicates. For example, application of HT (P) (P ∧ clock ≤ clock ) results in a healthy predicate that specifies there is no reverse time travel.
The observational variables and healthiness conditions give rise to a subset of the alphabetised relations called a UTP theory, which can be used to justify the fundamental theorems of a computational paradigm. A UTP theory is the set of fixed points of the healthiness condition: H H {P | H(P) = P}. A set of signature operators can then be defined, under which the theory's healthiness conditions are closed, and are thus guaranteed to construct programs that satisfy these theorems. UTP theories allow us to model a variety of paradigms beyond simple imperative programs, such as concurrency [43,55], real-time [62], object orientation [60], hybrid [28,27], and probabilistic systems [9].
The use of relational calculus means that the UTP lends itself to automated program verification using refinement S P: program P satisfies specification S. Since both S and P are specified in formal logic, and refinement equates to reverse implication, we can utilise interactive and automated theorem proving technology for verification. This allows application of tools like Isabelle/HOL to program verification, which is the goal of our tool, Isabelle/UTP [33].

Isabelle/HOL
Isabelle/HOL [52] is a proof assistant for Higher Order Logic (HOL). It consists of the Pure meta-logic, and the HOL object logic. Pure provides a term language, polymorphic type system, syntax translation framework for extensible parsing and pretty printing, and an inference engine. The jEdit-based IDE allows L A T E X-like term rendering using Unicode. An Isabelle theory consists of type declarations, definitions, and theorems, which are usually proved by composition of existing theorems. Theorems have the form of P 1 ; · · · ; P n =⇒ Q, where P i is an assumption, and Q is the conclusion. Proof in Isabelle is conducted by invocation of tactics, which provide various mechanisms for automating proof steps. The simplifier tactic, simp, rewrites terms using equational theorems of the form f (x 1 · · · x n ) ≡ y, where the right-hand side is smaller than the left-hand side. The auto tactic combines simp with deductive reasoning using introduction, elimination, and destruction rules. Isabelle also has the powerful sledgehammer proof method [7] which invokes external first-order automated theorem provers and SMT solvers on a proof goal, and internally verifies their results using tactics like simp and metis, which is a first-order resolution prover. Additional proof tactics and strategies can be constructed using the ML programming language.
The HOL object logic implements an ML-like functional programming language founded on an axiomatic set theory similar to ZFC. HOL is purely definitional: mathematical libraries of definitions and theorems are constructed purely by application of the foundational axioms in the proof kernel. This afford a highly principled approach to mechanised mathematics. HOL provides inductive datatypes, recursive functions, and records. Several basic types are provided, including sets (P A), total functions (A → B), numbers (N, Z, R), and lists. Parametric types are written by precomposing the type name, τ , with the type variables [α 1 , · · · , α n ]τ , for example [nat]list 1 . A notion of type specialisation allows two types to be unified if one can be expressed by instantiating the type variables of the other. For example, [nat]list specialises [α]list, where α is a type parameter.
Types in Isabelle/HOL correspond to non-empty sets. The fundamental command for defining new types is the typedef command, which creates a type, which is potentially parametric, based on a non-empty subset of an existing type. For example, if prime : N → B is a predicate that specifies whether or not a given number is prime, then we can create the type definition using the subset {n : N | prime(n)}, which requires that we can exhibit at least one prime number. Upon this foundation several specialised type definition commands exist. The datatype command creates an algebraic data type with a finite number of constructors. The record command creates a record type with a number of fields.
Isabelle also provides a number of facilities helpful in mechanisation of algebraic structures and specifications. Locales [5] provide axiomatic specifications of an algebraic structure in terms of (1) a number of abstract sort types, (2) a collection of signature operators over the sorts, (3) axioms that constrain the behaviour of the operators, and (4) theorems that follow from the axioms. For example, a semigroup structure can be specified in terms of (1) a single sort A, (2) a binary operator (· : A → A → A), (3) an associativity axiom ((x · y) · z = x · (y · z)), and (4) any theorems that follow. With such a structure defined, we can instantiate it with a particular concrete set of types and functions, provided that those functions can be proven to obey the axioms. For example, we could instantiate the semigroup locale with [A]list and the list concatenation function (xs ys), which is associative. Locales can also be arranged in a hierarchy, with child locales adding further operators and axioms. A related notion is type classes, which restrict locales to a single type sort, and use the polymorphic overloading function of Isabelle to characterise the algebraic operators. This for instance allows us to overload + with several definitions for different types.

Mechanising UTP
Mechanisation of the UTP involves constructing a tool that can aid the construction and verification of UTP theories, and put these to work in program verification. Most existing mechanisations [53,54,20] semantically embed the UTP into an existing logic, usually HOL, which allows them harness the latter's existing proof facilities. The exception is the U · (TP) 2 tool [11,12], a bespoke proof assistant for the UTP in the early stages of development. A semantic embedding of the UTP requires that we first model its fundamental model of computation: alphabetised relations [43,Chapter 2]. The model must both be faithful to the UTP, so that its pen-and-paper results can be mechanised, whilst also providing access to automated proof facilities of the host logic.
In the UTP book [43], an alphabetised relation is a pair (αP, P), where αP is a set of variable declarations, of the form x : t, and P is a predicate containing no free variables other than those in αP [43]. Intuitively, the alphabet consists of the selection of system properties that we wish to observe. As in the Z notation [63], a variable can be primed x , meaning that it is an output (or "after") variable. Then, the alphabet of a relation can be decomposed into the set of inputs and outputs, respectively: αP = inαP ∪ outαP.
Alphabets play a very important role in UTP by providing information that is used by programming operators to calculate the semantics of compositions. They are used in Chapter 2 to determine whether two sequentially executing programs P ; Q are compatible by ensuring that outαP = inαQ. In Chapter 7 (Concurrency), alphabets are used to determine whether two concurrently executing programs, P Q, manipulate disjoint regions of the memory through a proviso αP ∩ αQ = ∅. Moreover, alphabets are used to specify observational variables, and are thus important in giving a structure to UTP theories.
The earliest UTP mechanisation, created by Nuka and Woodcock [53], develops a deep embedding of the alphabetised relational calculus in ProofPower-Z, a proof assistant that builds on HOL. They develop an abstract syntax tree for predicates, a semantic domain, and an interpretation function. They utilise a semantic domain of the form Pred (P Var) × (P Binding), which is a product of an alphabet, that is a set of variable names, and a set of possible observations (Binding), which is modelled as a partial function from variables to values: Binding (Var → Value). This naturally means it is necessary to define types for both variables (Var) and values (Value). The set of observations is equivalent to a predicate over the observation space of type Binding → B.
The need for an abstract syntax tree for predicates is implied by UTP's definition of alphabetised relations [43], which depends upon a notation of free variables, a syntactic property of predicates. However, as pointed out by [54], fixing an abstract syntax tree runs against the UTP doctrine of having an extensible syntax to support various notations with a unified semantics. Consequently, Oliveira's mechanisation of UTP in ProofPower-Z [54] omits the abstract syntax tree, and instead defines operators directly on the semantic domain, which takes a similar form to Pred [53], resulting in a shallow embedding. The absence of an abstract syntax tree means that there is no longer a concept of free variables, which is sometimes used in the side conditions of programming laws. They solve this problem by defining a notion of "unrestriction", a semantic notion that a predicate does not depend on particular variables, an idea we adopt in Isabelle/UTP.
Oliveira's mechanisation [54] omits an explicit formalisation of types, which is often needed for alphabet declarations, and so Zeyda and Cavalcanti later extended that work with a type model and typing relation [68]. This proves to be essential for mechanising UTP theories, and their work develops a hierarchy of such theories, from imperative programs through to reactive programs. Two related shortcomings of this work, though, is the lack of support for native type checking and proof automation. Since the typing relation is formalised, it is necessary to prove typing side conditions, which hampers proof. This problem is alleviated in a following work [32], which provides an additional "shallow layer" of the predicate model that harnesses the Isabelle type system to discharge typing provisos. However, the work also places an additional burden on the user of defining their own Value type. Proof is also hampered by the need to discharge alphabet provisos. For example, a sequential composition P ; Q is well-formed only if outα(P) = inα(Q), a property which is not automatically checked and must be proved.
A different approach to the works above is taken by Feliachi et al. [20,21], who develop a UTP theorem prover in Isabelle/HOL. Like [53] and [54], they model predicates as sets of observations P S. However, S is not Binding, but any definable type in Isabelle/HOL. Generally, they use record types to encode observation spaces, where each field corresponds to a variable, and therefore proof automation is greatly improved in their tool. Their predicate type, [α]predicate is parametrised by an observation space type α. Moreover, by convention, the record type declarations double as alphabets, so that the type checker is directly harnessed in checking alphabet provisos. Specifically, the type [α]relation [α × α]predicate, denotes a homogeneous relation whose alphabet is α. Sequential composition has type [α]relation → [α]relation → [α]relation, and so relational compositions with incompatible alphabets are rejected.
Moreover, their approach can also harness type inference to automatically assign a polymorphic alphabet type to a relation. In textbook UTP, the assignment operator, x := A v, is decorated with an explicit alphabet A, which must be provided in order to infer the alphabet. This annotation is often omitted for convenience in [43], but this can only be done when the alphabet can be unambiguously inferred. By harnessing type inference, we can omit such explicit decorations, whilst obtaining relations that are wellformed by construction.
In addition to overcoming the problems with alphabets and types, [20,21] also overcomes the need for an explicitly formalised universe, Value, as required in the other works [53,54,68,32]. Since any type in HOL is required to have an a priori fixed cardinality, it is impossible to construct a type universe into which any HOL type can be injected. This is not a problem for [20,21], as predicates are parametric and an observation space type can make use of any HOL type for its variables. This problem is also alleviated in a further extension to the other works [69], so that we can have a distinguished type universe, but at the expense of extending HOL with additional axioms.
In our development of Isabelle/UTP, we broadly follow the direction taken by [20,21]. In particular we use the type system for alphabet inference as this greatly improves automation. However, we adopt several ideas from the other works [54,68,32], notably unrestriction, because the variable model in [20,21] does not permit us to form such properties of variables. In order to understand this, we need to look more closely at how observation spaces should be modelled. It turns out that these two families of mechanisations represent two unique approaches to modelling observation, which we consider next.

Observation Space Modelling
As we have seen, the principle difference between the UTP mechanisations is the approach to modelling the observation space S. These distinct approaches have been highlighted before in [61], which provides a general comparison. They identify four often employed models of observation, or state, in mechanised program models, namely (1) state as functions, (2) tuples, (3) records, and (4) abstract types, of which the first and third seem the most prevalent.
The first approach models observation as a function Var → Value, for suitable value and variable types. This approach is taken by [53,54,32,18,69], and requires a deep model of variables and values, in which concepts such as names and typing are first-class. This provides a highly expressive model with few limitations on possible manipulations [32]. However, [61] highlights two obstacles: (1) the machinery required for deep reasoning about program values is heavy and a priori limits possible constructions, and (2) explicit variable naming requires one to consider syntactic issues like substitution and α-renaming. Whilst [69] effectively mitigates (1), by axiomatically introducing a value universe, the complexities associated with (2) remain. Once names and types are treated as first-class, it becomes necessary to replicate a large portion of the underlying proof system meta-logic, which requires great effort and can hit proof efficiency. Nevertheless, the approach seems necessary to model dynamic creation of variables, as required, for example, in modelling memory heaps in separation logic [13,18].
The alternative approach uses records to model state; a technique often used by verification tools in Isabelle [1,20,21,2]. In particular, [20] uses this approach to create their semantic embedding of the UTP in Isabelle/HOL. A variable in this kind of model is represented simply by a record field. These can be abstractly represented using pairs of field-query and update functions, f i and f i -upd. The set of variable names (Var) therefore does not need to encoded in this approach. As shown in [20,21,2], this approach greatly simplifies automation of program verification in comparison to the former functional approach through directly harnessing, rather than replicating, the polymorphic type system and automated proof tactics. However, the expense is a loss of flexibility compared to the functional approach, particularly in regards to decomposition of state spaces. Moreover, those employing records seldom provide general support for syntactic concepts like free variables and substitution.
Isabelle/UTP employs an approach which generalises both these models by abstractly characterising the behaviour of state and variables algebraically using lenses. Consequently, it can achieve both a highlevel of proof automation like [20,21], but also support for syntax-like queries, such as unrestriction and substitution. Lenses were originally created as an abstraction for bidirectional programming and solving the view-update problem [23]. They abstract different views on a data space, and allow their manipulation independently of the context. A lens consists of two functions: get that extracts a view from a larger source, and put that puts back an updated view. [22] gives a detailed study of the algebraic lens laws for these functions. Combinators are also provided for composing lenses [24,23]. They have been practically applied in the Boomerang language 2 for transformations on textual data structures.
Our lens approach is indeed related to the state-space solution in [61] of using Isabelle locales to characterise a state type abstractly and polymorphically. A difference though is their use of explicit names, where our lenses are nameless. We also note that a very similar concept to lenses exists in Back's refinement calculus [3,Chapter 5], which substantially pre-dates the work on lenses. Here, get is called val, the "access function", and put is called set, the "update function", but the three lens axioms listed above are all present. A difference is that, unlike for lenses, [3] does not provide explicit models for the variable axioms.

Algebraic Observation Spaces
In this section, we present our theory of lenses, which provides an algebraic semantics for states and observation space modelling in Isabelle/UTP. Although some core definitions like the lens laws and composition operator are well known [24,23,22], we introduce several novel operators, like summation and quotient, and relations like independence and equivalence. This enables an algebraic approach to modelling of state spaces that is strongly related to the work of Back [3]. This section also constitutes a substantial expansion of materials in [33,Section 3] with a more precise presentation and several novel results.
As we have observed in §2.3, program variables are often modelled as opaque syntactic objects that necessitate a mixing of syntactic meta-logic concerns and program logic. Here, we will use lenses [24,23] to model variables as abstract behavioural semantic entities. Rather than fixing a particular model for variables, we simply require that the chosen model satisfies the lens axioms. Our contention is, therefore, that lenses provide a unifying solution to state space modelling.
All definitions, theorems, and proofs in this section may be found in our Isabelle/HOL mechanisation [30].

Signature
Lenses are a well-known mathematical concept, but here we will generalise them and recast several mathematical results. A lens is used, intuitively, to view and manipulate a V-shaped region of a larger source type S, as illustrated in Figure 3. We introduce lenses axiomatically as two-sorted algebraic structures. Definition 3.1 (Lenses). A lens is a quadruple V | S | get : S → V | put : S → V → S , where V and S are non-empty sets called the view type and source type, respectively, and get and put are total functions. We write V =⇒ S to denote the type of lenses with source type S and view type V, and subscript get and put with the name of a particular lens. We define create X v put X (εs • s ∈ S) v, which constructs an arbitrary source using Hilbert's choice operator (ε) and then puts v into it. The get function views the current value of the region, and put updates it. Intuitively, we will use these structures to model sequences of queries and updates on the state space S in §4. Each variable in a program can be represented by an individual lens, with operators like assignment utilising get and put to manipulate the corresponding region of program memory. The create function is usually axiomatised as a separate element of the lens signature, but here we prefer to define it in terms of put, which depends only upon S being non-empty. For the purpose of example, we describe lenses for record types.

Definition 3.2 (Record Lens).
Consider the definition of a new record type, R f 1 : τ 1 , · · · f n : τ n , which consists of n fields each having a corresponding type. Each field yields a function: f i : R → τ i which queries the current value of a field. Moreover, we can update the value of field f i in r : R with k : τ i using r(f i := k). We can construct a lens for each field using rec R fi The record lens allows us to employ "state as records" approach [61,20]. We also consider a second example. Many state spaces are built using the Cartesian product type S 1 × S 2 , and consequently it is useful to define lenses for a such a space. We therefore define the fst and snd lenses.

Definition 3.3 (Cartesian Product Lenses).
fst S1,S2 The subscripted source types are necessary in order to specify the product type; we will omit them when they can be determined from the context. Lenses fst and snd allow us to focus on the first and second element of a product type, respectively. Their get functions project out these elements, and the put functions replace the first and second elements with the given value z. A final example is the total function lens: The total function lens fun A,B k views the output of a function f : A → B associated with a given input value k : A. The get function simply applies f to k, and the put function associates a new output v with k. The function lens allows us to also employ the "state as functions" approach [54,61].

Axiomatic Basis
The crucial characteristic of lenses is that they allow manipulation of the data within a particular region of the source type, without affecting the data stored elsewhere. As we have previously shown, lenses therefore provide an effective method for giving behavioural semantics to program variables. The use of lenses to model variables depends on get and put behaving according to a set of axioms.
We write V =⇒ S for the set of total lenses with view type V and source type S, and * =⇒ S for the set of total lenses with any view type, whose source type is S.
We mechanise this algebraic structure in Isabelle using locales [5]. Total lenses are usually called "very well-behaved" lenses in the literature [24,23], but we believe "total" is more descriptive of the behaviour, since it is always possible to meaningfully project a view from a source. Axiom PutGet states that if a source has been constructed by application of put s v, then a matching get returns the injected value, v. Axiom PutPut states that a later put overrides an earlier one, so that the previously injected value v is replaced by v. Finally, Axiom GetPut states that for any source element s, if we extract the view element and then update the original using it then we get precisely s back.
We will now demonstrate that every field of a record yields a total lens.

Theorem 3.1.
For any field f i of a record type R, the record lens rec R fi forms a total lens. Proof. For illustration, we prove each lens axiom in turn.
Consequently, the record lens is indeed a total lens.
We can similarly show that fst, snd, and fun are total lenses 3 . Whilst both PutGet and PutPut are satisfied for most useful state-space models we can consider, this is not the case for GetPut. For example, if we consider a lens that projects the valuation of an element x : A from a partial function f : A → B, then get is only meaningful when x ∈ dom(f ). Since get is total, it must return a value, but this will be arbitrary and therefore placing it back into f will alter its domain. We can therefore also consider the set of partial lenses, that do not satisfy GetPut, but we will not consider this further for this paper in order to retain focus on the Isabelle/UTP core, but simply observe that total lenses are a useful, but not universal solution for state space modelling.
A useful subset of the total lenses are bijective lenses, as identified in [23,22]. We write X : V ⇐⇒ S, for X : V =⇒ S, if X is a bijective lens.
Axiom StrongGetPut states that application of get s retrieves a view that is to sufficiently large to entirely replace any preexisting source s with s . In other words, a bijective lens declares a kind of isomorphism between V and S, so that V must contain precisely the same level of information as is present in S. In state space terms, bijective lenses allow us to switch between equivalently expressive state space models. Clearly, any bijective lens is also a total lens, since StrongGetPut is more general than GetPut. In order to illustrate this, an example bijective lens is defined below.
The swap lens commutes the elements of a product space S 1 ×S 2 . Clearly then there is no loss of information associated with the get function. We prove that this lens satisfies axiom StrongGetPut below. Proof. We prove that both PutGet and StrongGetPut hold.

Independence
So far we have considered the behaviour of individual lenses, but programs reference several variables and so it is necessary to coordinate the semantics of the corresponding lenses. One of the most important relationships between lenses is independence of their corrensponding views, which is illustrated in Figure 4. We formally characterise independence below. Definition 3.8 (Independent Lenses). Lenses X : V 1 =⇒ S and Y : V 2 =⇒ S are independent, written X Y , provided they satisfy the following laws: Lenses X and Y , which share the same source type but not necessarily the same view type, are independent provided that their put functions commute (LI1), and their respective get functions are not influenced by the corresponding put functions (LI2, LI3). If X and Y are variables, then independence means that we can reorder assignments to them. We can, for example, show that fst snd using the calculation below.

Theorem 3.4. fst snd
Proof. We first prove that put fst commutes with put snd (LI1) by evaluation: Similarly, we can also prove LI2 by evaluation:  A further, illustrative, result is the meaning of independence in the total function lens: Two instances of the total function lens are independent if, and only if, the parametrised inputs a and b are different. This reflects the intuition of a function -every input is associated with a distinct output. This kind of independence property is also present in [3], though it is characterised as an assumption of variables with different names, rather than as a predicate to be used in assumptions of a modelled variable.

Combinators
In this section, we define an algebraic structure for lenses, beginning with some basic lenses. The 0 lens is a nominal lens that has a unitary view type, {∅}. Consequently, for any element of the source type, it always views the same value ∅. It cannot be used to either observe or change a source, and it is therefore entirely ineffectual in nature. Conversely, the 1 lens view, with type S =⇒ S, views the entirety of the source. The 0 and 1 lenses serve no practical purpose, but are useful units for the other functions.
. If X and Y are total independent lenses, then X + Y is a total lens.
Lens sum allows us to simultaneously manipulate two regions of the source S characterised by X : V 1 =⇒ S and Y : V 2 =⇒ S. Consequently, the view type is the product of the two constituents: V 1 × V 2 . The get function applies both constituent get functions in parallel. The put function applies the constituent put functions, but in sequence since we are in the function domain. We require that X Y , since manipulation of two overlapping regions could have unexpected results, and then also the order of the put functions is irrelevant. The sum operator can be used to characterise concurrent updates to the state space.
Another important operator is lens composition, which is a variant of an operator described in [23].
. If X and Y are total lenses, then X Y is a total lens.
A lens composition, X Y , for X : A =⇒ B and Y : B =⇒ C chains together two lenses. When X characterises an A-shaped region of B, and Y characterises a B-shaped region of C , overall lens X Y characterises an A-shaped region of C . It is useful when we have a state space composed of several individual state components, and we wish to select a variable of an individual component. We exemplify this below. Lens composition obeys a number of useful algebraic properties, as shown below. Theorem 3.9 (Lens Composition Laws). If X , Y , and Z are total lenses then the following identities hold: Lens composition is associative and has 1 as its left and right units, making it a monoid. Moreover, 0 is a left and right annihilator, since if the view is reduced to {∅} then no further information can be extracted. With the help of lens composition, we can now also prove some algebraic laws for lens sum. Theorem 3.10 (Lens Sum). If X and Y are independent total lenses then the following identities hold: The first two identities show that fst and snd composed with + yield the left-and right-hand side lenses, respectively. The third shows that swap indeed commutes +. The fourth shows that distributes from the right through lens sum. We next show some independence properties for the operators introduced so far. Theorem 3.11 (Independence). If X , Y , and Z are total lenses then the following identities hold: The 0 lens is independent from any lens, since it has no manipulative power. Lens independence is a symmetric relation, as expected. Lens composition preserves independence: if Y Z then composing X with Y still yields a lens independent of Z . X and Y composed with a common lens Z are independent if, and only if, X and Y are themselves independent. Finally, lens plus also preserves independence: if both X and Y are independent of Z , then also X + Y is independent of Z .

Observational Order and Equivalence
A lens X can view a larger region than another lens Y , with the implication that Y is fully dependent on X . For example, it is clear that in Example 3.1 each object fully possesses each of its attributes, and likewise each attribute lens x j o k is fully dependent on lens o k . We can formalise this using the lens order.
A lens X : V 1 =⇒ S is narrower than a lens Y : V 2 =⇒ S provided that they share the same source, and there exists a total lens Z : V 1 =⇒ V 2 , such that X is the same as Z Y . In other words, the behaviour is defined by firstly viewing the source using Y , and the secondly viewing a subregion of this using Z . An order characterises the size of a lens's aperture: how much of the source a lens can view. For example, we can prove that x j o k o k , by setting Z = x j in Definition 3.12. The lens order relation is a preorder. Theorem 3.12. For any S, ( * =⇒ S, ) forms a preorder, that is, is reflexive and transitive. Furthermore, the least element of * =⇒ S is 0 S , and the greatest element is 1 S .
Clearly, 0 is the narrowest possible lens since it allows us to view nothing, and 1 is the widest lens, since it views the entire source. We can prove the following intuitive theorem for sublens. Theorem 3.13. If X , Y are total lenses and X Y , then the following identities hold: Law LS1 is a generalisation of Axiom PutPut: a later put X overrides an earlier put Y when X Y . Law LS2 states when viewing an update on Y via a narrower lens X we can ignore the valuation of the original source, since the update replaces all the relevant information. We can now use these results to prove a number of ordering theorem for lens compositions. Theorem 3.14 (Lens Order Laws). If X , Y , and Z are total lenses then they satisfy the following laws: As we observed, composition of X and Y yields a narrow lens than Y (LO1). Independence is preserved by the ordering, since a subregion of a larger independent region is also clearly independent (LO2). Lens plus also preserves the ordering in its right-hand component (LO3). Moreover, lens plus is commutative with respect to (LO4), and also associative, assuming appropriate independence properties (LO5). From these laws, and utilising the preorder theorems, we can prove various useful corollaries, such as which shows that X is, of course, narrower than X + Y , and which shows that plus preserves the order in both its arguments. We can also induce an equivalence relation on lenses using the lens order.
Proof. Reflexivity and transitivity follow by Theorem 3.12, and symmetry follows by definition.
This ≈ relation is different to equality (X = Y ), since it requires only that the two sources types are the same, whilst the view types can be different. This makes this relation much more useful for evaluating observational equivalence between two lenses which have apparently differing views, and yet characterise precisely the same region. This is reflected by the following set of algebraic laws. Theorem 3.16 (Lens Algebra). If X , Y , and Z are all total lenses then they satisfy the following identities: Lenses thus form a partial commutative monoid [18], also known as a separation algebra [13], where X + Y is effectively defined only when X Y , which is a separateness relation.
We can also use lens equivalence to give the following alternative characterisation of bijective lenses.

Theorem 3.17. X is a bijective lens if, and only if, X ≈ 1
A bijective lens is equivalent to 1, meaning that its view type contains exactly the same amount of information as the source type. We can use this fact to describe the partitioning of a state space by two independent lenses: X + Y ≈ 1. This characterises the notion of lens complements [23], where the view types of X and Y represent complementary regions of the source. Similarly, we can use bijective lenses to establish an equivalence relation between lenses: An equivalence between X and Y can be established if we can find a bijective lens which when composed with Y , yields X . Lens Z can be viewed as an adaptor from one lens to the other.

Mechanised State Spaces
The algebraic theory of lenses described in this section is mechanised in Isabelle/HOL [30]. We will now show how it provides the basis for state spaces in our program verification framework in Isabelle/UTP. Manual construction of state spaces using the lens combinators is tedious and so we also implement an Isabelle/HOL command for automatically creating a new state space with the following form: It creates a new state space type S, and a lens for each of the variables x i : τ i . It can be used to describe a concrete state space for a program. For brevity, we often abbreviate the alphabet command by the syntax when used in mathematical definitions. Internally, the command performs the following steps: 1. generate a record space type S with n fields, which optionally extends an existing state space T ; 2. generate a lens x i for each of the fields using the record lens rec R xi ; 3. automatically prove that each lens x i is a total lens; 4. automatically prove an independence theorem x i x j for each pair i, j ∈ {1 · · · n} such that i = j; 5. generate lenses base S and more S that characterise the "base part" and "extension part", respectively; 6. automatically prove a number of independence and equivalence properties.
We will now elaborate on each of these steps in detail.
The new record type S yields an auxiliary type (α 1 , · · · , α k , φ) S-ext with additional type parameter φ that characterises future extensions. In particular, the non-extended type (α 1 , · · · , α k ) S is characterised by (α 1 , · · · , α k , unit) S-ext, where unit is a distinguished singleton type. This extensible record type is isomorphic to a product of three basic component types: These characterise, respectively, the part of state space described by T , the part described by the n additional fields, and the extension part φ. In the case that the state space does not extend an existing type, we can set (β 1 , · · · , β m ) T = unit.
For each field, the command generates a lens x i : τ i =⇒ (α 1 , · · · , α k , φ) S-ext using the record lens, and prove total lens and independence theorems. Each of these lenses is polymorphic over φ, so that they can be applied to the base type and any extension thereof, in the style of inheritance in object oriented data structures. As we show in §6, this polymorphism allows us to characterise a hierarchy of UTP theories.
The base part consists of only the inherited fields and those added by S. We automatically prove a number of theorems about these special lenses: • base S more S : the base and extension parts are independent; • base S + more S ≈ 1: they partition the entire state space; • for i ∈ {1 · · · n}, x i base S : each variable lens is part of the base; • base S ≈ base T + i∈{1···n} x i : the base is composed of the parent's base and the variable lenses; • more T ≈ i∈{1···n} x i + more S : the parent's extension is composed of the variable lenses and the child's extension part.
These theorems support the Isabelle/UTP laws of programming, which we elaborate in the next section.

Mechanising the UTP Relational Calculus
In this section we will describe the core of Isabelle/UTP, including its expression model, meta-logical operators, predicate calculus, and relational calculus, building upon our algebraic model of state spaces. A direct result is an expressive model of relational programs which can be used in proving fundamental algebraic laws of programming [44], and for formal verification ( §4). Moreover, the relational model is foundational to the mechanisation of UTP theories, and thus advanced computational paradigms, such as reactive programming, which we consider in §6.

Expressions
Expressions are the basis of all other program and model objects in Isabelle/UTP, in that every such artefact is a specialisation of the expression type. An expression language typically includes literals, variables, and function symbols, all of which are also accounted for here.
We model expressions as functions on the observation space: where A is the return type, which is a similar approach to that taken in [3]. There is no inductively defined abstract syntax tree for expressions, but simply a collection of definitions that allow composition of expressions using HOL functions. Our model therefore technically represents a shallow embedding [8,20], but it nevertheless supports expression of a variety of syntax-like constraints using lenses.
A major advantage of this model is that we need not preconceive of all expression constructors, but can add them by definition. Using Isabelle/HOL's type definition (typedef ) mechanism we obtain both a new type [A, S]uexpr, and a function, − e : [A, S]uexpr → S → A, that obtains the characteristic function from an expression. We also obtain the following foundational extensionality principle: We can demonstrate that two expressions e and f are equal provided that their characteristic functions yield the same value for any state space s. We now show how the core calculus for expressions is constructed.
and assign these constants the following semantic definitions: The operator var x represents a variable expression, and returns the present value in the state characterised by lens x. For convenience, we assume that x, y, z, and decorations thereof, are lenses, and will often use them directly as variable expressions without explicitly using var. We will also use v to denote the 1 lens; this is effectively a special variable for the entire state.
The operator lit k represents a literal, or alternatively an arbitrary lifted HOL value, and corresponds to a constant function expression. We use the notation k to denote a literal k. As well as lens-based variables, which are used to model program variables, expressions can also contain HOL variables, which are orthogonal and constant with respect to the program variables. HOL variables in literal constructions can be used to represent meta-variables, for example x , which are something necessary in proof about programs. We use the notations x, y, and z to denote logical variables in expressions.
Operator cond b u 1 u 2 denotes a conditional expression; if b is true then it returns u 1 , otherwise u 2 . It evaluates the boolean expression b under the incoming state, and chooses the expression based on this. We will use the notation e u 1 u 2 as a short hand for it.
Operators uop and bop lift HOL functions into the expression space by a pointwise lifting. With them we can transparently use HOL functions as UTP expression functions, for instance the summation e + f is denoted by bop (+) e f . Moreover, it is often possible to lift theorems from the underlying operators to the expressions themselves, which allows us to reuse the large library of HOL algebraic structures in Isabelle/UTP. For instance, if we know that (A, +, 0) is a monoid, then also we can show that for any S, ([A, S]uexpr, bop (+), lit 0) forms a monoid. For convenience, we therefore often overload mathematically defined functions as expression constructs without further comment. In particular, we will often overload = as both equivalence of two expressions (e = f ), and an expression of equality within an expression (x = 5).

Predicate Calculus
A predicate is an expression with a Boolean return type, [S]upred [B, S]uexpr, so that predicates are a subtype of expressions. Then, the majority of predicate calculus operators can be obtained by pointwise lifting of the equivalent operators in HOL. In order to notationally distinguish the latter, in the following definitions we subscript them with a H.
The propositional calculus operators (¬, ∧, ∨, ⇒) are simply defined by pointwise lifting. We define two pairs of quantifiers, since we have both logical variables and lenses in Isabelle/UTP. Quantifiers ∀ and ∃ universally and existentially quantify lens x by universally quantifying over possible values, v, and updating x with them. The dual quantifiers ∀ and ∃, which are notationally emboldened, quantify a logical variable in a parametric predicate P(x) by a direct lifting of the corresponding HOL quantifier. The universal closure, [P], universally quantifies every variable in the alphabet of P using the state variable v. The refinement relation P Q is then defined as a HOL predicate, requiring that Q implies P in every state s.
In addition to the binary operators ∧ and ∨, we also define the corresponding indexed operators.

Definition 4.3 (Indexed Operators).
i∈A The definitions are by lifting of the underlying HOL operators, and therefore we obtain the following theorem. As usual, via the Knaster-Tarski theorem, for any monotonic function F : [S]upred → [S]upred we can describe the least and greatest fixed points, µ F and νF , which in UTP are called the weakest and strongest fixed points, and obey the usual fixed point laws. We can also algebraically characterise the UTP variable quantifiers using Cylindric Algebra [39], which axiomatises the quantifiers of first-order logic.
From this algebra, the usual laws of quantification can be derived [39]. These laws illustrate the difference in expressive power between HOL and UTP variables. For the former, we cannot pose meta-logical questions like whether two variable names x and y refer to the same region, such as may be the case if they are aliased. For this kind of property, we can using lens independence x y, as required by laws C6 and C7. Lenses can model both individual variables, and also larger regions of the state space formed by summation of several (x + y). We can therefore model finite sets of variables, and thus quantification over multiple variables such as ∃ x, y, z • P, which is represented as ∃ x + y + z • P, and then prove the following laws.
Theorem 4.4. If A and B are total lenses, then the following identities hold: Ex1 shows that quantifying over two disjoint sets of variables equates to quantification over both. Disjointness of variable sets is modelled by requiring that the corresponding lenses are independent. Ex2 shows that quantification over a larger lens subsumes a smaller lens. Finally Ex3 shows that if we quantify over two lenses that identify the same subregion then those two quantifications are equal. We now have a complete set of operators and laws for the predicate calculus; next we will show how proof can be mechanically automated.

Automated Proof
The approach to define the operators of the predicate calculus using pointwise lifted HOL operators allows us to harness Isabelle/HOL's automated proof tactics. The strategy is to transfer an equality or refinement conjecture about UTP predicates to an equivalent one about HOL predicates using the interpretation function e e . The resulting proof tactic, which we called rel-auto, employs the following steps to attempt discharge a goal of the form e = f : 1. apply a transfer rule, such as Theorem 4.1, to obtain a goal of the form e e s = f e s; 2. evaluate e e s and f e s to HOL terms using interpretation rules, such as Definitions 4.1 and 4.2; 3. apply the auto tactic to invoke automated simplification and deduction.
The strategy is not always successful, and so residual proof obligations may be left afterwards. In this case, it is possible to apply the sledgehammer [7] tactic on the resulting proof obligations, or alternatively the nitpick counterexample generator. We permit the set of semantic interpretation rules used by step (2) to be expanded by additional definitional equations, so that the proof strategy is extensible. The example calculation below shows how the proof strategy can be used for a simple predicative conjecture.
The crucial observations from this example are that (1) UTP variables are compiled to expressions of the form get x s, and (2) all other operators simply become their HOL equivalents. Of course, x and y can be any lens into the state space S, which is an arbitrary type.
The proof procedure is enhanced when S is constructed using the alphabet command of §3.6, because we can enumerate all the field lenses. Given a state space [x 1 : τ 1 , · · · x n : τ n ], we can eliminate the s state space variable in a proof goal by replacing it with a tuple of HOL variables (x 1 · · · x n ). This, in turn, means that we can eliminate each lens expression and replace it with a corresponding HOL variable, so that the example above, when transferred, simply becomes that is, every UTP variable has been replaced by a corresponding HOL variable, which means that we can directly and without reference to lenses invoke HOL proof procedures. This approach means that we have both the additional expressivity and fidelity afforded by lenses, and the proof automation of Isabelle/HOL. In the next section we explore some of the advantages of using lenses rather than HOL variables directly.

Meta-Logic
Lenses allow us to treat variables as semantic object that can be checked for independence, ordered, and composed in various ways. As we have noted, we can consider such manipulations as meta-logical with respect to the predicate. We will now add further specialised meta-logical queries for expressions.
Often we want to check which parts of the state space an expression depends on, for example to support laws of programming and verification calculi. Though this is often characterised syntactically using free variables, here we follow [54] and characterise it semantically with the "unrestriction" operator.
Intuitively, e is unrestricted by lens x, written x e, provided that e's valuation does not depend on x. Specifically, the effect of e evaluated under state s is the same if we change the value of x. It is thus a sufficient notion to formalise the meta-logical provisos for the laws of programming. Below are some key laws for establishing whether an expression is unrestricted by a variable. x y x u y u (x + y) u x y x (∃ y • P) x y x P x (∃ y • P) x y x (∀ y • P) x y x P x (∀ y • P) Expression lit k does not depend on the state since it always returns k; consequently it is unrestricted by any lens x. Expression var x is unrestricted by any lens y that is independent from x. The laws for uop and bop require simply that the component expressions are unrestricted by lens x. No expression is restricted by the 0 lens, since it characterises none of the state-space. Unrestriction is preserved by the lens order . An expression u is unrestricted by the summation of lenses x and y provided that x and y are independent, and the expression is unrestricted by both u and v. Again, we note that + can effectively be used to group lenses in order to characterise a set of variables.
Aside from checking for use of variables, UTP theories often require that the state space of a predicate can be extended with additional variables. An example of this is the variable block operator that adds a new local variable. In Isabelle/UTP, alphabets are implicitly characterised by state space types, rather than explicitly as sets of variables. Consequently, we perform alphabet extensions by manipulation of the underlying state space using lenses. We define the following operators to extend a state space. Alphabet extrusion, e ⊕ p a, uses the lens a : S 1 =⇒ S 2 to extend the state space of e : [A, S 1 ]uexpr to become S 2 . The lens effectively describes how one state space can be embedded into another. For example, let us assume we have a state space composed of two sub-regions: S A×B. Then, a predicate P : [A]upred, that acts on state space A, can be coerced to one acting on S by an alphabet extrusion: P ⊕ fst : [S]upred. Naturally, we know that the resulting predicate is unrestricted by the B region.
Alphabet extrustion has no effect on a literal expression, other than to change its type, because it refers to no lenses. A variable constructor has its lens augmented by composing it with the alphabet lens a. The extrusion simply distributes through unary and binary expressions.

Substitutions
Deterministic programs can be modelled as total functions σ, ρ : S → S that transform an initial state to a final state. Such programs are conceptually substitutions, since they define the valuation for each program variable in terms of a current value. The simplest substitution, id (λ x • x), leaves the state unchanged. We define operators for querying and updating substitutions below.
Substitution query σ s x : [A, S]uexpr returns the expression associated with x : A =⇒ S in σ : S → S by composition of the latter with get x . Substitution update assigns the expression e to the lens x in σ. The definition constructs a function that inputs the state s, evaluates e with respect to s, calculates the state space updated by σ, and then uses put to update the value of x in σ(s) with the evaluated expression. We can then introduce the short-hand [x 1 → s e 1 , · · · , x n → s e n ] id(x 1 → s e 1 , · · · , x n → s e n ) which constructs a substitution in n variables that assigns the expression e i to each variable x i . This notation will allow to model multiple variable assignment, and also evaluation contexts for programs and expressions.
We also prove a number of laws about substitutions constructed from maplets.
Theorem 4.7. If x and y are total lenses, then the following identities hold: The majority of these reflect the intuition of substitution queries and updates. Law SB4 states that two substitution maplets, x → s e and y → s f , are commutable provided that x and y are independent. Similarly, SB5 states that a later assignment for y overrides an earlier assignment for x when y is a wider lens than x. This is, of course, true in particular when x = y.
Substitutions can be sequentially composed using the composition operator ρ • σ (λ x • ρ(σ(x))), meaning ρ after σ. Conditional choices can be expressed using the following construct. A conditional substitution is equivalent to σ when b is true, and ρ otherwise. The definition evaluates b under the incoming state s, and then chooses which substitution to apply based on this. Substitutions can be applied to an expression using the following operator.
Application of σ to a variable x is the valuation of x in σ (SA1). A substitution maplet for an unrestricted variable can be removed (SA2). Substitutions distribute through both unary (SA3) and binary (SA4) operators. A singleton substitution for variable x can pass through an existential quantification over y provided that x and y are independent, and e is unrestricted by y (SA5), which prevents variable capture. Application of id has no effect (SA6), and application of two substitutions can be expressed by their composition (SA7). SA8 shows that when σ is composed with another substitution composed of maplets (x → s e), it is simply applied to the expression e of every such maplet. SA9 shows how two substitutions with matching maplets can be conditionally composed, by distributing the conditional.
As for expressions, we define an operator to extend the alphabet of a substitution. We use the lens a : S 1 =⇒ S 2 to coerce σ : S 1 → S 1 to the state space S 2 . The resulting substitution first obtains an element of S 1 from the incoming state s : S 2 using get a , applies the substitution to this, and then places the updated state back into s using put a . This is the essence of a framed computation; the parts of s outside of the view of a are unchanged.

Relational Calculus
A relation is a predicate on a product space S 1 × S 2 , specifically, where S 1 and S 2 are the state spaces before and after execution, respectively. All laws that have been proved for expressions and predicates therefore hold for relations. We define types for both heterogeneous relations, [S 1 , S 2 ]urel [S 1 × S 2 ]upred, and homogeneous relations [S]hrel [S, S]urel. Operators true and false can be specialised in this relational setting, and stand for the most and least non-deterministic relations. Due to their special role, we will use the notation true and false to explicitly refer to these relational counterparts.
In common with formal languages like Z and B, UTP uses the notional convention for variables that x is the initial value and x is its final value. The former can be denoted by the lens composition x fst, and the latter by x snd, where x is actually the name of a lens of type τ =⇒ S. In this presentation we define the operators below for lifting variables, expressions, and substitutions into the product space. x x fst x x snd e e ⊕ p fst e e ⊕ p snd σ σ ⊕ s fst σ σ ⊕ s snd The and lift a lens, expression, or substitution, into the first and second components of a product state space S 1 × S 2 . Operator e lifts an expression e : [A, S 1 ]uexpr to an expression on the product state space S 1 × S 2 , for any given S 2 . If e is a predicate on the state variables, then e is a predicate on the initial state, that is a precondition. Similarly, e constructs a postcondition with state space S 1 × S 2 from e : [A, S 2 ]uexpr. The analogous operators σ and σ lift a substitution to the product space.
We can now define the main programming operators of the relational calculus.
These broadly follow the common definitions given in relational calculus and the UTP book [43], but with subtle differences due to our use of lenses. Relational composition P ; Q existentiality quantifies a HOL meta-variable v 0 that stands for the intermediate state between P and Q. It is substituted as the final state of P (using v ), and the initial state of Q; the resulting predicates are then conjoined. Composition is a heterogeneous operator of type [S 1 , Relational identity (I I), or skip, equates the initial state with the final state, leaving all variables unchanged. σ is a generalised assignment operator constructed using a substitution σ : S → S. Its definition states that the final state is equal to the initial state with σ applied. The substitution σ can be constructed as a set of maplets, so that a singleton assignment x := v can be expressed as x → s v , and a multiple variable assignment as x 1 → s v 1 · · · x n → s v n . Since x can be any kind of lens in an assignment, we can encode array assignment a[i] := v, which updates the index i in array a to have value v, whilst leaving the remainder of a unchanged. An array over type A, with size n + 1, can be modelled as a total function with a finite domain: {0 · · · n} → A 4 . The array lens a[i] can then be denoted using fun Conditional P b Q states that if b is true then behave like P, otherwise behave like Q. In the UTP book [43] the fact that b acts on initial variables is a syntactic convention, whereas here this wellformedness condition is imposed by construction using b . For completeness, we use this operator, and the fact that all predicates, including relations, form a complete lattice, to define the while loop operator b P. We use the strongest fixed-point, ν, as we will use it for partial correctness verification in §5. We now have all the operators of a simple imperative programming language, and can prove the laws of programming [44,43].
The majority of these are standard, and therefore we select only a few for commentary. LP10 would normally require as a proviso that b is an expression in initial variables only, but in our setting this fact follows by construction. LP4 is a generalisation of the forward assignment law: an assignment by σ followed by relation P is equivalent to σ applied to the initial variables of P. The more traditional formulation [44,43], x := e ; P = P[e/x], is an instance of this law. Similarly, LP5 is a generalised conditional assignment law which combines σ and ρ into a single conditional substitution. All the other assignment laws can be proved, but we need some additional properties for relational substitutions, which are shown below.
shows that a precondition substitution applies only to the first element of a sequential composition, and RS2 is its dual. RS3 shows that precondition substitution applied to an assignment can be expressed as a composite assignment. RS4 shows that σ applied to a conditional distributes through all three arguments. The precondition annotation is removed when applied to b since this is a precondition expression already. The combination of Theorems 4.8, 4.9, and 4.10 allows us to prove the classical assignment laws [44]. Using these laws we can collapse any sequential and conditional composition of assignments into a single assignment, as shown in [44]. In addition to the deterministic programming operators, we can formulate the following specification operators below.

Definition 4.12 (Specifications
A non-deterministic choice over an indexed relation, i∈A • P(i), can simply be expressed using the predicative disjunction operator. We note that, by Theorem 4.2, any set of relations [S 1 , S 2 ]urel forms a complete lattice, where is the least upper bound. As usual, we write P Q for the simpler binary case. The relational converse P • , inverts the direction of a relation by application of swap as an alphabet extrusion. This swaps the first and second components of the product state space.
We will now explore the algebraic properties that our relational model satisfies, beginning with quantales.
A corollary of this result is that UTP relations over S also form Kleene Algebra with P * = (νX • P ; X I I). This allows us link to a large body of well known results in algebraic automated verification [2]. We also show that UTP relations for a Relation Algebra [64]; a key algebraic structure for program specifications.
We have therefore now constructed the relational calculus, and shown that its operators satisfy a large number of important algebraic structures, which validates its correctness. In the next section, we will use these theorems to construct symbolic execution and verification facilities for relational programs.

Automated Verification of Relational Programs
In this section we demonstrate how the programming foundations established in §3 and §4 can be applied to automated program analysis. We show how concrete programs can be modelled, symbolically executed, and automatically verified using mechanically validated operational and axiomatic semantics.

Encoding Programs
Imperative programs can be encoded using the operators given in §4, and a concrete state space with the required variables. For example, we can describe the factorial algorithm as shown below: Constant pfact is a function taking a natural number X as input and producing a program of type [sfact]hrel that computes the factorial. The given value is assigned to UTP variable x, and 1 is assigned to y. Then, the program iteratively multiplies y by x, and decrements x. In the final state, y will have the factorial.
We use this as a running example for the Isabelle/UTP symbolic execution and verification components.

Symbolic Execution
The UTP book [43] characterises a small-step operational semantics for the relational imperative program languages using a step relation: (s, P) → (t, Q). Here, we adopt a similar idea to describe a reduction semantics for relational programs, and use it to perform symbolic execution. We begin by describing the execution of a program P started in a state context Γ. The meaning of Γ |= P is that program P is executed in the context of variable context Γ, which gives assignments to the variables of S, for example [x → s 5, y → s true]. The expression Γ |= I I denotes a program that has terminated in state Γ. The definition of the operator is very simple, because of our encoding of variable contexts as substitutions: we apply Γ as an assignment, and compose this with the program P. Using this definition we can prove a set of reduction theorems.
The arrow P → Q actually denotes an equality predicate (P = Q); we use the arrow notation to aid in comprehension, and to emphasise the left-to-right nature. The first two rules on the top line handle sequential composition. The first pushes an evaluation into the first argument of a composition P ; Q. The second rule states that when the first argument of a sequential composition has terminated (I I), execution moves on to the second argument (P). The third rule handles assignments by creating a new context by precomposing the assignment σ with the current context. The second and third lines deal with conditional and while loop iteration, respectively. In all these rules, the context Γ is applied to the condition b as a substitution. If the result is true, the conditional chooses the first branch P, and the while loop makes a copy of the loop body. If the result is false, the conditional chooses the second branch Q, and the while loop terminates.
Using these theorems, we can perform symbolic execution of programs in Isabelle/UTP. To achieve this we load the Isabelle simplifier with both the equations of Theorem 5.1 and also those of Theorem 4.8, the latter of which allows us to apply substitutions. We also utilise the pointwise lifted semantics given in §4.1 to evaluate expressions using the builtin HOL functional definitions and simplification laws.
In addition, we need the equations of Theorem 4.7 to evaluate and normalise substitutions. However, Law SB4, which allows reordering of subsitution maplets, is symmetric and therefore cannot be directly used as it would cause the simplifier to loop. The issue is that lenses do not apriori have a total order that can be used to reorder them. Nevertheless, Law SB4 is important to enable a canonical representation of concrete substitutions. Consequently, we extend the simplifier with a "simproc" [52], a specialised meta-logical simplification procedure that sorts substitution maplets lexicographically using the syntactic lens names. Thus, during symbolic evaluation the variable context will always order the variables lexicographically.
Applying the Isabelle simplifier with these laws, we can symbolically execute programs. Below, we give an example execution of the factorial program from Example 5.1. We do this by using the simplifier to evaluate the term id |= pfact(4), where id encodes an arbitrary initial assignment for all the variables. = [x → s 1, y → s 24] |= I I In this case, the program terminates in final state [x → s 1, y → s 24], but in the case of a non-terminating program the simplifier will loop. Such a symbolic execution engine is a useful tool for simulation of programs. In the next section we show how we can also verify programs.

Program Verification
A Hoare triple {b} P {c} is an assertion that, if program P is started in a state satisfying predicate b, then all final states satisfy predicate c. The UTP book [43] shows how this assertion can be encoded using a refinement statement. The definition in Isabelle/UTP is given below.

Definition 5.2 (Hoare Triple). {b} P {c} ((b ⇒ c ) P)
This definition states that the Hoare triple is valid when P is a refinement of the relational specification b ⇒ c . An alternative characterisation is given in terms of our reduction relation is given below.
This is an example of a linking theorem that relates two semantic presentations, in this case how the Hoare triple is related to the operational semantics. The satisfaction of {b} P {c} implies that, for any initial state assignment Γ 1 satisfying precondition b, if P terminates with final state assignment Γ 2 , then Γ 2 satisfies c. Thus we have formally related the operational and axiomatic semantics for relational programs. From Definition 5.2 we can also prove, as theorems, the following Hoare calculus laws: The majority of these laws are standard. However, the formulation of the assignment law is more general than the standard law, {p[e/x]} x := e {p}. It avoids the aliasing problem of classical Hoare logic since substitution depends on semantic independence of lenses, rather than syntactic inequality of variable names.
We can use these laws to automatically verify our factorial program. We require, as usual, that the program is annoted with loop invariants. The proof strategy, implemented in the Isabelle/UTP tactic hoare-auto, executes the following steps: 1. Combine all composed assignments using Theorem 4.11. 2. Apply the Hoare logic laws of Theorem 5.3 as deduction rules. 3. Perform any substitutions in the resulting predicates using Theorems 4.7 and 4.8. 4. Apply the rel-auto tactic of §4.3 to each resulting predicate.
The result is a set of HOL predicates that characterise the verification conditions for the program. We exemplify this with the factorial program below.

Theorem 5.4. {true} pfact(X) {y = X !}
Proof. Application of hoare-auto yields the following verification conditions: In this case, both proof obligations can be discharged using sledgehammer.
Thus we have shown how Isabelle/UTP can be applied to practical verification of relational programs. In the next section we will consider verification of languages based on advanced computational paradigms.

Advanced Verification Tools
In this section we show how advanced verification tools can be constructed using Isabelle/UTP theories. We first describe how UTP theories are characterised in Isabelle/UTP, and illustrate their utility in §6.1. We then describe a small reactive programming language in §6.2, outline a hierarchy of UTP theories for characterising reactive programs in §6.3, and assign our language a denotational semantics and algebraic theorems in §6.4, which we utilise in §7 to provide a denotational semantics and verification tool for RoboChart [48]. Finally in §6.5, we show how proof support for UTP theories can be optimised for efficient automated reasoning. Our mechanisation adds further rigour to these theories, and enables their use in verification.

Isabelle/UTP Theories
The relational program model we constructed in §4 is powerful, but not without limitations. It is well known, for instance, that basic relations cannot adequately characterise non-terminating behaviour [16]. Furthermore, several programming paradigms, such as real-time, concurrency, and object orientation, require a richer semantic model with more observable information [16,60,62].
This semantic enrichment is facilitated by UTP theories. Additional semantic information is expressed by adding special observational variables, which encode quantities of a program or model, and invariants that restrict their domain, called healthiness conditions. The observational variables can be used to define specialised operators for a particular computational paradigm, such as a delay or deadline operator for a real-time language. The healthiness conditions allow us to impose well-formedness invariants over these observational variables, and allow us to prove algebraic theorems that characterise the healthy elements. As usual, healthiness conditions are represented as idempotent predicate transformers, that is, functions on relations over the observational variables.
We characterise UTP theories in Isabelle/UTP as follows: We mechanise this algebraic structure using locales [5]. The type [α]T characterises the observations that can be made of the model. Since it can be parametric, it characterises a set of possible ground observation types, which instantiate all the type parameters. An observation space can be constructed using the alphabet command ( §3.6), in which case it defines a set of lenses, x 1 · · · x n , which are the observational variables. The healthiness conditions are encoded as total endofunctions on homogeneous relations parameterised by [α]T . If a theory has multiple healthiness conditions, then these can be composed function-wise. The simplest UTP theory is the relational theory, Rel (α, λ X • X ). Any observation type is an instance of α, and any relation is a fixed-point of λ X • X .
We say that a relation P : [[α]T ]hrel is H-healthy, written P is H, when P is a fixed-point: H(P) = P. Moreover, we characterise the healthy elements of a theory by the set H H {P | P is H}. Idempotence of H ensures that the UTP theory is non-empty since for any relation P, H(P) ∈ H H . To illustrate, we formalise the UTP theory for timed relational programs introduced in §2.1. ensures that time monotonically advances. HT is clearly idempotent, since conjunction is idempotent. We define the following operator for introducing a delay for timed relations: Here, clock is advanced by n, and the state is unchanged. We can prove that wait(n) is HT -healthy, since it advances time. Conversely, the predicate clock = clock − 1 is not healthy, since it tries to reverse time.
As in previous work [20,68], our theories form "families": they characterise relations on several observation spaces the the observation type is potentially polymorphic, and thus extensible with additional variables. For example, our theory in Example 6.1 is parametric in S. We can characterise a subtheory relation between UTP theories: Subtheories allow us to arrange theories in a hierarchy with descendants that specialise the observation space with additional variables and constraints. UTP theories also include a signature: a set of operators that construct healthy elements of the theory. We say that an operator in n parameters, is in the signature if H H is closed under F . Formally, we require that: The function F can either denote a new operator defined on [α]T , or an existing operator defined over a parent observation space. For example, nondeterministic choice P Q and sequential composition P ; Q often inhabit the signature of several theories, since they are typed by arbitrary relations and so can be instantiated by any observation space. This also means that the corresponding algebraic laws for a parent operator F can be directly applied to elements of a new subtheory. For example, sequential composition is always associative, since every theory is a subtheory of Rel.
We exemplify this by giving the signature of our theory of timed relations.
Once the signature operators have been established, the final step is to prove the characteristic algebraic theorems for them. These laws effectively provide an algebraic semantics for the UTP theory, and can be used to aid in the construction of program verification tools. There are three ways to obtain such theorems in Isabelle/UTP. Firstly, we can inherit them from a parent theory by utilising Definition 6.2. Secondly, we can import them from an algebraic structure by proving the latter's axioms. Thirdly, we can prove them manually using Isabelle/UTP's proof tactics.
We exemplify the third approach for the new delay operator, using our rel-auto proof tactic ( §4.3): Waiting for a zero length duration is simply a skip operation (I I), sequential composition of two delays, by m and n time units, is equivalent to a single m + n delay. A delay distributes through a conditional provided that b does not refer to the clock variable. A delay commutes with an assignment provided that the delay and assigned expressions can be independently evaluated.
Algebraic theorems for UTP theories can also be obtained by linking to a variety of mechanised algebraic structures. The HOL-Algebra library [6], for example, characterises the axioms of partial orders, lattices, complete lattices, Galois connections, and the myriad of theorems that can be derived from them. A substantial advantage of the UTP approach is that algebraic theorems can often be reduced to proving properties of the underlying healthiness conditions, which allows us to obtain laws with minimal effort. We exemplify this by restricting ourselves to a particular subclass of continuous UTP theories.

Definition 6.3.
H is continuous provided that H( i∈A P(i)) = i∈A H(P(i)) whenever A = ∅.
In a continuous theory, the healthiness condition distributes through arbitrary non-empty relational infima. A corollary of this definition is that H is also monotonic: P Q ⇒ H(P) H(Q). Then, by the Knaster-Tarski theorem, also part of HOL-Algebra, we can show that H H forms a complete lattice under refinement . This allows us to import theorems for recursive and iterative programs into a UTP theory.
From the induced complete lattice, we obtain the following operators: infimum T , supremum T , top element T , bottom element ⊥ T , and least fixed-point µ T , which are all in the theory's signature, and for which the usual complete lattice and fixed-point calculus theorems [4] hold. Moreover, in a continuous UTP theory, these operators can be calculated using the equational theorems given below.

Theorem 6.3 (Continuous Theory Properties).
These theorems demonstrate the relationship between the theory operators, and the relational ones defined in §4. The theory top and bottom elements are the relational top and bottom with H applied. The theory infimum T A is T when A is empty, and otherwise the relational infimum. Moreover, the least fixed-point operator can be expressed as the relational least fixed-point by precomposition of H. The utility of these theorems is that we can construct non-deterministic choices and recursive programs using the relational operators and µ, which again allows reuse of their algebraic laws.
We now demonstrate how we can obtain such theorems for timed relations.

Theorem 6.4. HT is continuous, since conjunction distributes through disjunction ( ). We therefore obtain a complete lattice, and can calculate the top and bottom element:
We also obtain a least fixed-point operator for constructing and reasoning about iteration, µ rt , and can use it to denote a timed loop operator: b rt P (µ rt X • P ; X b I I).
From these theorems, we could now proceed to define a timed Hoare calculus and proof tactics following the template given in §5. A concrete timed program can be modelled by creating a suitable state space, vars [x 1 : τ 1 · · · x n : τ n ], defining the program P : [[vars]rt]hrel using the signature operators, and proving that P is HT . Finally, the proven Hoare logic deduction rules can be used for program verification.
We have demonstrated how a UTP theory can be mechanically validated, a set of signature operators verified, and algebraic theorems for these operators proved. Next, we apply this approach to a more substantial hierarchy of UTP theories for reactive programs.

Reactive Programs
The theory of reactive designs [43,16] provides a generic semantic foundation for reactive programs. It demonstrates how UTP can be applied to integration of formal methods by semantic unification. At its core, the theory combines two computational paradigms: state-and event-based modelling. It grew out of a twenty year endeavour [67,34,59,43,54] to obtain a theory that can unify state-based notations, like Z, B, and refinement calculus, with event-based notations, like process calculi CCS, CSP, and π-calculus.
Reactive designs have notably been used to give a denotational semantics to the Circus language family [54], that integrates operators from Z, Dijkstra's guarded command language [17], and CSP [41]. Extensions of Circus exist that utilise the theory unification facilities of UTP to characterise further paradigms like real-time [62,65] and object-orientation [60]. In our more recent work, we have further generalised the theory of reactive designs with an abstract trace model [27,26] that unifies all the aforementioned extensions, and also hybrid dynamical systems with continuous variables. In this work, we use reactive designs to mechanise a denotational semantics of, and verification support for, a reactive action language, which is summarised below. We use this language in §7 to, in turn, give a denotational semantics to basic RoboChart state machines. We assume existing syntactic categories for identifiers (ID) and expressions (Expr), both of which can be provided by Isabelle/UTP. In this definition, {P} denotes replication of P zero or more times. The language combines communication and sequential programming constructs. The basic constructs include visible events, skip, deadlock (Stop), assignment, and sequential composition. Events are used to communicate with the environment. An event can either be a basic synchronisation (a), an input event (a?x) which receives a value over channel a and populates variable x with it, or an output event (a!v) that sends a value over a. A guarded action b & P, behaves like P if predicate b is true, and otherwise deadlocks. An external choice P 2 Q allows the environment to pick whether P or Q is activated, depending on their initial events offered. Finally, an action system, do b 1 P 1 | · · · | b n P n od , iteratively executes one of the P i actions, based on those that have a true guard. If no guard is true, the action system terminates. The iteration operator is important as it allows us to encode the transition relation in a RoboChart state machine in §7. We give an informal example of the use of this language in describing a buffer. The variable bf , which stores the buffer contents, is initially set to the empty sequence ( ). The buffer then repeatedly offers to input a value over the channel inp, and extend bf with it, or else when the buffer is not empty (#bf > 0), output the first element of the buffer of the output channel out. The true guard in the iteration means that this action never terminates, which is usual for reactive programs.

Reactive Designs Theory Hierarchy
We give an overview of the mechanisation of the reactive design hierarchy, which consists of several UTP theories, namely designs [43,15], reactive processes [43,27], stateful reactive designs [26], and stateful failure reactive designs [54,29], which extends the predicative semantics of CSP with state. The observation spaces and healthiness conditions of these theories are summarised in Table 1. For reasons of space, we do not elaborate the details of the healthiness conditions, which have been thoroughly explained and presented elsewhere [43,15,26,29], but concentrate on their mechanisation in Isabelle/UTP. The following list gives the intuition of the conceptual layers, which is illustrated in Figure 6. 1. Designs extend the relational program model with the possibility of erroneous or "divergent" behaviour. If a program diverges, it becomes unpredictable, which corresponds to unspecified behaviour.

UTP Theory
Observation   (2) quiescent behaviour, where the program is awaiting interaction from the environment. Quiescence can occurs when waiting for an external input, such as a message. 3. Stateful Reactive Designs introduce an explicit program state variable (st), require that this is cannot be observed in quiescent observations, and combine designs and reactive processes to represent programs that can both quiesce and diverge. As illustrated by the red arrows in Figure 6, it is constructed by effectively embedding designs into reactive processes, which theories are otherwise disjoint. 4. Stateful Failure Reactive Designs additionally encode a CSP-style refusal set in every quiescent observation, which is intuitively used to indicate the events that are enabled.
The layering of UTP theories allows the reuse of laws that are proven at each level of specialisation. Here, we focus on the specialisation to stateful failure reactive designs, but reactive designs can also be specialised with real-time, probabilistic, or hybrid dynamical behaviour. There are two kinds of specialisation that can be made. The first is extension of the observation space with extra variables, which resembles inheritance, and the second is the subtheory relation of Definition 6.2. Both kinds of extension are utilised in summary Table 1. We now summarise how the layers of theory are built up in Isabelle/UTP.
The theory of designs [43] has observation space type des, and healthiness condition H, itself composed of H1 and H2 [43]. The type of H is [φ]des-ext → [φ]des-ext, where [φ]des-ext is the polymorphic extension type (cf. §3.6). The φ parameter means that it is applicable to any extension of observation space des. The lens ok : B =⇒ [φ]des-ext is used as a flag that allows us to observe whether a program, or its predecessor, is proceeding normally or has diverged. Healthiness condition H1 ensures that no program variables can be observed until the program has been started (ok ). H2 ensures that no program can require divergence. The signature constructor for designs is P Q (ok ∧ P) ⇒ (ok ∧ Q), which constructs a program with a precondition (P) and a postcondition (Q). The postcondition Q characterises successful and terminating observations, whilst P denotes the conditions of valid execution: if P is violated, then the design diverges.
The reactive processes [27] observation space [T ]rp, extends des with observational variables wait and tr. These are used to observe, respectively, whether a program is quiescent, that is, waiting for interaction from the environment, and the current trace history. Variable ok is inherited, and its type specialised to B =⇒ [T ]rp. The type parameter T , from which tr draws its type, denotes a particular trace model [29], such as a sequence of events or a piece-wise continuous function. In Isabelle/HOL, we enforce a polymorphic sort constraint on T which ensures that the core operators of trace algebra [27] are defined on T , and the associated axioms proved. The theory of reactive processes does not inherit the healthiness conditions of designs, but defines its own: R1 and R2 5 . R1 requires that the trace variable is monotonically extended, so no event can be "undone", and R2 prevents a program's behaviour from depending on events that occurred before it began executing. Intuitively, these two healthiness conditions give rise to a special variable tt, which is equivalent to tr − tr, and is used to encode the traces contributed by a process [26].
Stateful reactive designs is a subtheory of reactive processes that adds a state lens st : S =⇒ [S, T ]rsp. This allow characterisation of the program variables with lenses of type τ =⇒ S. The healthiness condition is NSRD, which extends R with R3 h , SRD1 , and SRD3 6 . R3 h ensures that st is unobservable in quiescent phases: if a predecessor to P is quiescent (wait ), then the program behaves like I I R , the reactive identity, or else it behaves like P. The theory also includes reactive versions of the design healthiness conditions, and effectively embeds designs into reactive processes. Specifically, SRD1 composes H1 with R1 , so that divergent behaviour allows arbitrary extension of the trace. SRD3 requires the the reactive design skip I I R is a right unit, and is analogous to H2 .
Embedding designs into reactive designs allows the specification of programs that have both divergent (erroneous) observations, which corresponds to violation of the precondition, and quiescent observations. The main specification operator in the reactive designs signature is [ P 1 -| P 2 | P 3 ], which constructs a reactive contract specification like a design, with a precondition P 1 and postcondition P 3 , but also an additional part (P 2 ), called a "pericondition" to characterise quiescent observations [26]. Specifically, any NSRD-healthy relation corresponds to a reactive contract triple. Moreover, our previous results [26,29] show that reactive programs can usually be reduced to reactive contracts of this from that specify the program's behaviour using three large predicates. If this is the case then we can verify whether an implementation contract satisfies an abstract specification using the following theorem [26]: provided the precondition is weakened, P 1 ⇒ Q 1 , the pericondition is stengthened, Q 2 ∧ P 1 ⇒ P 2 , and the postcondition is stengthened, This kind of contract-based verification is implemented in an Isabelle/UTP tactic called rdes-refine [26], which invokes the rel-auto tactic described in §4.3, and is analagous to our Hoare logic tactic hoare-auto from §5 but with a much enriched notion of specification. In this work, we do not consider reactive contracts further, but rather point the reader to companion publications [26,29]. The crucial observation is that these contracts facilitate an axiomatic semantics, based on refinement, that can be used for verification.
The reactive designs healthiness condition NSRD is continuous, and therefore we can utilise Theorem 6.3 to obtain a complete lattice, including a fixed-point operator µ R , and can use to construct non-deterministic choices. We call the top element of the lattice Miracle, since it denotes an unimplementable reactive program, and the bottom element Chaos, the most non-deterministic reactive program.

Definition 6.5. Miracle NSRD(false)
Chaos NSRD(true) The Miracle and Chaos elements are defined, following Theorem 6.3, by application of NSRD to false and true, respectively. We redefine the conditional operator, P b r Q, using alphabet extrusion by st to ensure that b may only refer to state variables, and not other variables like ok and tr, which could render the operator unhealthy. As defined, P b r Q is NSRD-healthy, provided that P and Q both are. The operator is defined in terms of the standard conditional operator from Definition 4.11, which, in particular, means that the relevant laws from Theorem 4.9 are applicable in this setting. Moreover, with the help of Theorem 6.3, we can obtain additional laws: Finally, the theory of stateful failure reactive designs adds the observational variable ref to encode refusals, and two additional healthiness conditions to govern them, which are composed in NCSP. These healthiness conditions essentially ensure that ref is only referenced in quiescent observations, and that ref is never mentioned, since a process should never depend on a predecessor's refusal set. Since NCSP specialises NSRD, any general law of reactive designs, such as those in Theorem 6.6, are inherited. We also note that Miracle, Chaos, and b r remain in the signature of NCSP, and therefore all their laws are applicable in this specialised theory. We can now use this theory to denote the reactive language shown in Definition 6.4.

Denotational Semantics of Reactive Programs
In this section we will show how the mechanisation of stateful failure reactive designs can be applied to give a denotational semantics to a reactive programming language. We will define both the CSP-style communication operators, and imperative operators similar to those found in Dijkstra's guarded command language [17]. We also prove crucial algebraic theorems, which can be used in program verification. Notably, we define the guarded iteration operator, and an induction law that can be used to support verification using refinement. We first define the following basic operators for reactive programs.
where As for the relational model, we define a generalised assignment operator σ c , which is parameterised by a substitution σ on S. The definition lifts σ into the reactive design observation space [S, E]sfrd using substitution extension (see Definition 4.9). It then constructs a relational assignment, and applies NCSP to produce a reactive design. As before, we can construct a singleton assignment x := v by lifting a singleton substitution: x → s v c . Moreover the lens results in §3, including the variable models, remain valid here. For example, we can use constructs like object structures and arrays ( §4.6) in this context.
The do(e) operator describes an event, represented by an expression e : [E, S]uexpr, based on the current state s : S. It generalises several event operators, including CSP event prefix, which can be defined as so: e → P (do(e) ; P). Its definition states that the operator does not diverge (ok ), and conjoins this with a predicate that describes the quiescent and terminated observations. In quiescent observations (wait ), the trace remains unaltered and the event e is not being refused. In terminated observations, (¬wait ), the trace is finally extended by e, and the state remains unchanged [16].
The b P operator denotes a "naked" guarded command [51]. Its behaviour is P when b is true, and miraculous otherwise, meaning it is impossible to execute. By Theorem 6.6, Miracle is a left annihilator for sequential composition, and so any behaviour following is excluded when b is false. An assumption [b] guards Skip with b, and thus holds all variables constant when b is true, and is otherwise miraculous. We also define the reactive while loop b r P, which is analogous to the relational version (Definition 4.11). NCSP H is closed under these three operators since they are defined only in terms of healthy elements · , Miracle, Skip, and µ R . We can also prove a set of theorems for these operators [29].
Theorem 6.7. If P and Q are NCSP-healthy, then the following identities hold: For brevity, we have omitted the definition of external choice which can be found elsewhere [29]. The first four of these identities are direct counterparts of relational laws in Theorem 4.9. Moreover, since these laws reduce assignment compositions to substitutions, we can also utilise Theorems 4.7 and 4.8 in this context. This, in particular, means we also obtain counterparts to all the assignment laws of Theorem 4.11.
Next, we add Dijkstra's alternation operator [17] to our model.
Alternation is a nondeterministic choice of guarded commands. When b(i) is true for i ∈ I , P(i) can be executed. Any command which has b(i) false reduces to Miracle and thus is eliminated. If no b(i) is true, then its behaviour is Chaos. If multiple b(i) are true then one of the corresponding P(i) is nondeterministically selected. NCSP H is closed under alternation since it is constructed from only healthy operators. From this definition we can prove a number of characteristic laws. Theorem 6.8. If, ∀ i • P(i) is NCSP, then the following identities hold: In words, (1) shows that alternation over an empty set presents no options, and so is equivalent to Chaos; (2) shows that a singleton alternation can be rewritten as a binary conditional; (3) shows that, if we assume that one of its branches is true, then an alternation degenerates to a nondeterministic choice. We now define the guarded iteration operator as the iteration of the corresponding alternation whilst at least one of the guards remains true.
We use the reactive while loop (b r P) to encode the operator, and can thus utilise our previous results [29] to reason about it. In keeping with the reactive programming paradigm, this while loop can pause during execution to await interaction, and it also need not terminate. However, in order to ensure that the underlying fixed point can be calculated, we assume that for all i ∈ I , P(i) is productive [27]: that is, it produces at least one event whenever it terminates. This ensures that divergence caused by an infinite loop is avoided. Iteration is closed under NCSP H , since the while loop and alternation both are. We summarise the healthy reactive programming operators in the closure theorem below. Theorem 6.9 (Stateful Failure Reactive Designs Signature).
To complete our theory, and enable verification support for iterated reactive programs, we prove the following fundamental refinement law for iteration. Theorem 6.10 (Iteration Induction). If, ∀ i • P(i) is NCSP, then: The law states the provisos under which an iteration, with initialiser I , preserves invariant S. These are: (1) every branch is productive; (2) if I causes the iteration to exit immediately then S is satisfied; (3) for any i ∈ A if I holds initially, b(i) is true, and P(i) executes, then S is satisfied (base case); and (4) for any i ∈ A, if S holds initially, b(i) is true, and P(i) executes, then S is satisfied (inductive case). This law forms the basis for our verification strategy for state machines that we utilise in §7.

Proof Optimisation
We complete the discussion of UTP theories by showing how, once constructed, they can be optimised for use in automated verification tools. The approach to theory engineering we have described above has several advantages [43,16]. There is a unified notion of refinement that can be applied across semantic domains. Operators like nondeterminsitic choice ( ) and sequential composition (;) can occupy several theories, which facilitates generality and semantic integration. General algebraic laws can be proved, and then directly reused in more specialised UTP theories, for example reactive process and reactive design laws can be specialised to stateful failure reactive designs. The UTP approach also means that theories can be both combined and extended for a wide variety of computational paradigms and languages.
However, there is a practical downside, which is that the programming theorems, such as those in Theorem 6.7 and 6.6, depend on our showing healthiness of the constituent parameters, and therefore it is necessary to first invoke a set of closure theorems. In the context of verification, constantly proving closure can be very inefficient, particularly for larger programs. This is because Isabelle's simplifier works best when invoked with pure equations f (x 1 , · · · , x n ) ≡ y with minimal provisos.
Our solution uses the Isabelle type system to shoulder the burden of closure proof. We use Isabelle's typedef mechanism, which creates a new type T from a non-empty subset A :: P(U ) of existing type U . For a UTP theory, we create a type with A = H H , which is a subset of the UTP relations. This then allows optimised proof for a particular UTP theory, but at the cost of generality and semantic extensibility which are more suited to the UTP relational domain.
In order to obtain the signature for the new type, we utilise the lifting package [45], whose objective is to define operators on T in terms of operators on U , provided that A is closed under each operator. Specifically, if f is a signature operator in k arguments, then we can create a lifted operator f :: T k → T using Isabelle's lift-definition command [45]. This raises a proof obligation that f ∈ H k H → H H , which can be discharged by the corresponding closure theorem. Programs constructed from the lifted operators are well-formed by construction.
Finally, to lift the algebraic theorems for each lifted operator f , we use the transfer tactic [45]. It allows us to prove theorems like f (P 1 , · · · , P k ) = g(P 1 , · · · , P k ), where P i :: T is a free variable, by converting it to a theorem of the form Q 1 is H ∧ · · · ∧ Q k is H =⇒ f (Q 1 , · · · , Q k ) = g(Q 1 , · · · , Q k ). This means the closure properties of each parameter Q i can be utilised in disharging provisos of the corresponding UTP theorems, but the lifted theorems do not require them. We use this technique for our reactive program type.
Using Isabelle's typedef mechanism, we define a new type [S, E]action to encode reactive programs, which is isomorphic to NCSP H , and a subset of the type [[S, E]sfrd]hrel. We then use the lifting package to create constructors corresponding to each of the signature operators in Theorem 6.9. This means that the type system of Isabelle ensures that reactive programs constructed using these operators are healthy by construction. The final step is to transfer each of the laws given in Theorems 6.7, 6.6, 6.8, and 6.10 to the new [S, E]action domain. This result is a set of algebraic theorems without closure provisos, which can then be applied directly as part of our verification procedure. In this section we have demonstrated the mechanisation of UTP, demonstrated their use in constructing a reactive program theory hierarchy, and showed how the resulting laws can be optimised for verification. In the next section we finally apply this to verification support for RoboChart state machines.

Automated Verification of State Machines
In this section we draw together the collected results from sections 3, 4, and 6 to construct an automated verification tool for the graphical state machine notation, RoboChart, in Isabelle/UTP. We begin by describing the RoboChart language in more detail, and then proceed to construct the tool in Isabelle.

RoboChart
RoboChart [48,47] describes robotic systems in terms of a number of controllers that communicate using shared channels. Each controller has a well defined interface, and its behaviour is described by one or more state machines. A machine has local state variables and constants, and consists of nodes and transitions, with behaviour specified using a formal action language [55]. Advanced features such as hierarchy, shared variables, real-time constraints, and probability are supported.
A machine, GasAnalysis, is shown in Figure 7; we use it as a running example. It models a component of a chemical detector robot [40] that searches for dangerous chemicals using its spectrometer device, and drops flags at such locations. GasAnalysis is the component that decides how to respond to a sensor reading. If gas is detected, then an analysis is performed to see whether the gas is above or below a given threshold. If it is below, then the robot attempts to triangulate a position for the source location and turns toward it, and if it is above, it stops.
The interface consists of four events. The event gas is used to receive sensor readings, and turn is used to communicate a change of direction. The remaining events, resume and stop carry no data, and are used to communicate that the robot should resume its searching activities, or stop. The state machine uses four state variables: sts to store the gas analysis status, gs to store the present reading, ins to store the reading intensity, and anl to store the angle the robot is pointing. It also has a constant thr for the gas intensity threshold. RoboChart provides basic types for variables and constants, including integers, real numbers, sets, and sequences (Seq(t)). The user can also define additional types, that can be records, enumerations, or entirely abstract. For example, the type Status is an enumerated type with constructors gasD and noGas.
The behaviour is described by 6 nodes, including an initial node (i); a final node (F ); and four states: NoGas, Analysis, GasDetected, and Reading. The transitions are decorated with expressions of the form trigger[condition]/statement. When the event trigger happens and the guard condition is true, then statement is executed, before transitioning to the next state. All three parts can optionally be omitted. RoboChart also permits states to have entry, during, and exit actions. In our example, both Analysis and GasDetected have entry actions.
Modelling with RoboChart is supported by the Eclipse-based RoboTool 7 , from which Figure 7 has been captured. RoboTool automates verification via model checking using FDR4, and its extension to incorporate the verification approach presented here is ongoing work.

Static Semantics
In this section we formalise the static semantics of state machines in Isabelle/HOL, which describes the variables, transitions, and nodes. The meta-model, presented below, is based on the untimed subset of RoboChart, but note that our use of UTP ensures that our work is extensible to more advanced semantic domains [62,9,27]. For now we omit constructs concerned with interfaces, operations, shared variables, during actions, and hierarchy, and focus on basic machines. It declares four fields for the initial state identifier (init), final states identifiers (finals), nodes definitions (nodes), and transition definitions (transs), and constitutes the static semantics. Since this corresponds to the meta-model, and to ensure a direct correspondence with the parser, we do not directly use sets and maps, but only lists in our structure. We will later derive views onto the data structure above, that build on well-formedness constraints.
Below, we show how syntactic machines are translated to Isabelle definitions.

Definition 7.3 (Static Semantics Translation).
statemachine s vars x 1 : τ v 1 · · · x i : τ v i events e 1 : τ e 1 · · · e j : τ e j states s 1 · · · s k initial ini is created, and lenses for each field of the form τ v i =⇒ s-alpha. For the events, an algebraic datatype s-ev is created with constructors corresponding to each of them. We create a distinguished event that will be used in transitions that not specify an explicit trigger event, which ensures that every transition has at least one visible event. This in turn ensures that the resulting reactive program is productive, as required by Theorem 6.10. The overall machine static semantics is then contained in machine. We also define semantics that contains the dynamic semantics in terms of the semantic function · M that we describe in §7. 3.
Elements of the meta-model are potentially not well-formed, for example specifying an initial state without a corresponding state declaration, and therefore it is necessary to formalise well-formedness. RoboTool enforces a number of well-formedness constraints [49,47], and we here formalise the subset needed to ensure the dynamic semantics given in §7.3 can be generated. We need some derived functions for this, and so we define nnames set(map nname (nodes)), which calculates the set of node names, and fnames, which calculates the set of final node names. We can now specify our well-formedness constraints.

Definition 7.4.
A state machine is well-formed if it satisfies these constraints: 1. Each node identifier is distinct: distinct(map nname (nodes)) 2. The initial identifier is defined: init ∈ nnames 3. The initial identifier is not final: init / ∈ fnames 4. Every transition's source node is defined and non-final: ∀ t ∈ transs • src(t) ∈ nnames \ fnames 5. Every transition's target node is defined: ∀ t ∈ transs • tgt(t) ∈ nnames We have implemented these constraints in Isabelle/HOL, along with a proof tactic called check-machine that discharges them automatically when a generated static semantics is well-formed, and ensures that crucial theorems are available to the dynamic semantics. In practice, any machine accepted by RoboTool is well-formed, and so this tactic simply provides a proof of that fact to Isabelle/HOL.
In a well-formed machine every node has a unique identifier. Therefore, using Definition 7.4, we construct two finite partial functions, nmap : ID → [s, e]Node and tmap : ID → [s, e]Transition list, that obtain the node definition and list of transitions associated with a particular node identifier, respectively, whose domains are both equal to nnames. We also define ninit nmap init, to be the definition of the initial node, and inters to be the set of nodes that are not final. Using well-formedness we can prove the following theorems. 1. All nodes are identified: ∀ n ∈ set(nodes) • nmap (nname(n)) = n 2. The initial node is defined: ninit ∈ set(nodes) 3. The name of the initial node is correct: nname(ninit) = init These theorems allow us to extract the unique node for each identifier, and in particular for the initial node. Thus, Isabelle/HOL can parse a state machine definition, construct a static semantics for it, and ensure that this semantics is both well-typed and well-formed. The resulting Isabelle command is illustrated in Figure 8 that encodes the GasAnalysis state machine of Figure 7.

Dynamic Semantics
In this section we describe the behaviour of a state machine using the reactive program domain we mechanised in §6.3. The RoboChart reference semantics [49,47] represents a state machine as a parallel composition of CSP processes that represent the individual variables and states. Variable access and state orchestration are modelled by communications between them. Here, we capture a simpler sequentialised semantics using guarded iteration, which eases verification. In particular, state variables have a direct semantics, and require no communication. The relation between these two semantics could, in the future, be formalised by an automated refinement strategy that reduces parallel to sequential composition [55].
We , e]action, extends the state space of P using lens a. It is similar to a frame in refinement calculus [51], which prevents modification of variables, but also uses the type system to statically prevent access to them. Lens a identifies a subregion s 2 , which P acts upon, of the larger observation space s 1 . Intuitively, s 2 specifies the set of state machine variables, and s 2 extends it with actv. P can only modify variables within s 2 , and others are held constant. We prove laws for this operator, which are also used in calculating the semantics. Frame extension distributes through sequential composition. For operators like event receive and assignment, the variable is extended by the lens a using a lens composition x a (see Def. 3.11), which we denote using a namespace-style operator (a:x). Specifically, it manipulates the region characterised by x within the region of a.
We now describe the dynamic semantics of a state diagram using three functions. final node is selected, then the iteration terminates. In each iteration, the node N that is named by actv is selected, and the semantics for it is calculated using M |= N N . When in a node, the entry action is first executed using nentry, and then an external choice is presented over all transitions associated with N , which are calculated using tmap. The entry and exit actions do not have actv in their observation space, and therefore we apply frame extensions to them. The semantics of a transition, M , N |= t T , is guarded by the transition condition, and awaits the trigger event. Once this occurs, the exit action of N is executed, followed by the transition action, and finally actv is updated with the target node identifier.
The output of the semantics is an iterative program with one branch for every non-final state. To illustrate, we below generate the denotational semantics for the GasAnalysis state machine given in Figure 7. In order to yield a more concise definition, we have also applied the action equations, given in Theorem 7.2 and §6.4, as simplification laws. In particular, the frame extensions have all been expanded so that the state variables are explicitly qualified by lens r . In order to verify such state machines, we need a specialised refinement introduction law. Using our well-formedness theorem, we can specialise Theorem 6.10. 3. calculate denotational semantics, resulting in a reactive program; 4. perform algebraic simplification and symbolic evaluation (Theorem 6.7); 5. apply Theorem 7.3 to produce sequential refinement proof obligations; 6. apply rdes-refine to each goal, which may result in residual proof obligations; 7. attempt to discharge each remaining proof obligation using sledgehammer [7]. This is effectively an elaborated version of the workflow followed by the rel-auto tactic we described in §4.3. Diagrammatic editors, like RoboTool, can be integrated with the proof tool by implementing a serialiser for the underlying meta-model. The workflow can be completely automated since there is no need to enter manual proofs, and the final proof obligations are discharged by automated theorem provers. If proof fails, Isabelle/HOL has the nitpick [7] counterexample generator that can be used for debugging. This means that the workflow can be hidden behind a graphical tool.
We can use the verification procedure to check deadlock freedom of a state machine using the reactive contract dlockf [ true -| ∃ e • e / ∈ ref | true ], an invariant specification which states that in all quiescent observations, there is always an event that is not being refused. In other words, at least one event is always enabled; this is the meaning of deadlock freedom. We can use this contract to check the GasAnalysis state machine. For a sequential machine, deadlock freedom means that it is not possible to enter a state and then make no further progress. Such a situation can occur if the outgoing transitions can all be disabled simultaneously if, for example, their guards do not cover all possibilities.
The result of applying the verification procedure up to step 5 is shown in Figure 9. At this stage, the semantics for each node has been generated, and deadlock freedom refinement conjectures need to be proved. Isabelle generates 6 subgoals, 3 of which are shown, since it is necessary to demonstrate that the invariant is satisfied by the initial state and each non-final state. The first goal corresponds to the initial state, where no event occurs and the variables gs and anl, along with actv, are all assigned. The second goal corresponds to the Analysis state. The state body has been further simplified from the form shown in Figure 7.1, since symbolic evaluation has pushed the entry action through the transition external choice, and into the two guards. This is also the case for the third goal, which corresponds to the more complex GasDetected state.
The penultimate step applies the rdes-refine tactic to each of the 6 goals. This produces 3 subgoals for each goal, a total of 18 first-order proof obligations, and invokes the relational calculus tactic rel-auto on each of them. The majority are discharged automatically, but in this case three HOL predicate subgoals remain. One of them relates to the Analysis state, and requires that the constructors noGas and gasD of Status are the only cases for sts. If there was a third case, there would be a deadlock as the outgoing transition guards don't cover this.
Finally, we execute sledgehammer on each of the three goals, which provides proofs and so completes the deadlock freedom check. Thus, we have engineered a fully automated deadlock freedom prover for state machines.

Conclusions
In this paper we have given a comprehensive exposition of the foundations of our verification tool framework, Isabelle/UTP. As we have demonstrated, Isabelle/UTP provides a unified semantic foundation for a variety of computational paradigms and programming languages, with the ability to formulate machine checked semantic models. These semantic models can then be harnessed in constructing verification tools that harness the powerful automated proof facilities of Isabelle/HOL.
We began this journey in §3 by describing how variables can be modelled as algebraic objects using lenses. This allows us to unify and compose a variety of variable models, and define generic operators for their comparison and manipulation. The lens-based model, in particular, allows us to avoid dependence on syntax, and instead build upon semantic properties like independence and containment.
We then used this algebraic observation space foundation in §4 to develop a flexible relational model including expressions, predicates, and alphabetised relations. Our fundamental expression model is a shallow embedding, which means it can directly harness the existing libraries of mathematical types and functions in Isabelle/HOL, and the associated theorems and proof strategies. We therefore provided a proof tactic for relational conjectures (rel-auto), and a library of algebraic theorems. In contrast to previous work, our expression model additionally supports syntax-like manipulations, including substitution and unrestriction, without the need for explicit modelling of variable names. It therefore offers both efficient automated proof on the one hand, and expressivity on the other hand.
We used the relational model to develop programming operators, and prove the "laws of programming" [44] as theorems, along with the axioms of several algebraic structures, like complete lattices, cylindrical algebra, and relation algebra. We then used this body of laws in §5 to provide symbolic execution and Hoare logic verification components for modelled relational programs.
We then showed, in §6, how the relational model can be specialised to particular computational paradigms with mechanised UTP theories. We showed how UTP theories are represented, in terms of observation spaces and healthiness conditions. Our theory model supports reuse of algebraic laws by a notion of inheritance, whereby a UTP theory can be extended with additional observational quantities and refined by further healthiness conditions. We showed how further laws can be obtained with links to algebraic structures.
We then used our mechanisation of UTP theories, in §6.3, to construct the reactive design theory hierarchy, which provides the semantic foundation for reactive programming languages. We used the specialised theory of stateful failure reactive designs to give a denotational semantics to a reactive programming language, with both state and interaction, and proved a number of important algebraic laws, including a verification law for iteration. We then showed how such a UTP theory can be optimised for proof automation, so that its algebraic laws can be efficiently applied to a modelled program.
Finally, in §7, we applied all of the aforementioned results in constructing a prototype verification tool for RoboChart state machine diagrams. We showed how the static semantics of the language can be mechanised as a collection of data types and well-formedness constraints, which Isabelle/HOL can check. We then showed how to mechanise the dynamic semantics, as an iterated system of guarded actions, using the reactive program model defined in §6. We then demonstrated a proof tactic that allows verification using invariants, and applied this to show that an example state machine is free from deadlock.
In conclusion, we believe that we have made the first steps toward realising the UTP vision [43, Chapter 0] of integrated formal methods, underpinned by unifying semantics. In many ways, this is only the beginning, as there remains a large number of computational paradigms that are not yet represented in Isabelle/UTP. A major item for future work is the mechanisation of the various pen-and-paper UTP theories that have been developed by the UTP community over the past twenty years [43,15,60,62,9]. Referring back to Figure 1, we are currently working on various UTP theories to support verification of C code, differential equations, and control law block diagrams, as well as enhancing the current support we have for RoboChart.
With respect to C code, one of the major features needed is a model of dynamically allocated memory addressed by pointers. We hinted back in §3.2 that we can weaken the axioms of total lenses to describe "partial lenses". A partial lens is only defined for a subset of the possible states, which can be used to distinguish allocated and dangling pointers. We are currently using this idea to mechanise separation logic [58] in Isabelle/UTP, and hope to report on this soon. With respect to differential equations, and hybrid dynamical systems, we have previously described an extension of the relational calculus with continuous variables [28,27]. The generic trace model of reactive designs [27] ( §6.3) and our extensible mechanisation of UTP theories means that we can specialise the reactive design hierarchy in a different direction to describe hybrid reactive systems, where the trace is a piecewise continuous function. We believe this can be applied, for instance, to assign a UTP semantics to a language like Hybrid CSP [35], which integrates continuous evolution with discrete CSP-style events and concurrency. Proof support for such a language depends on the ability to reason about invariants of differential equations, and so we are also integrating Platzer's differential induction technique [57], as employed by the KeYmaera tool 8 , into Isabelle/UTP. Moreover, we have previously given a UTP semantics to the dynamical systems modelling language Modelica [28], and so we will also develop proof facilities for this.
With respect to RoboChart, we will expand our semantics to handle additional features. Hierarchy, can be handled by having the actv variable hold a list of nodes, and during actions by implementing a reactive interruption operator [46]. Moreover, we are developing reasoning facilities for parallel composition and hiding to allow expression of concurrent state machines, which extends our existing work [26,29]. This will increase verification capabilities for robotic and component-based systems, and allow us to handle asynchronous communication and shared variables, and also to mechanise the CSP reference semantics [49].
A challenge that remains is handling assumptions and guarantees between parallel components, but we believe that abstraction of state machines to invariants, using our results, can make this tractable. We will also explore other reasoning approaches, such as use of the simplifier to algebraically transform state machines to equivalent forms. Going further, we emphasise that our UTP theory hierarchy supports more advanced semantic paradigms. We will therefore develop a mechanised theory of timed reactive designs, based on existing work [62,27], and use this to denote the timing constructs of RoboChart state machines. We are developing a UTP theory of probability [9], and will use it to handle probabilistic junctions. We also have our theory of hybrid reactive designs [28,27], which can support state machines with hybrid dynamics.