key: cord-0061027-q6ad465u
authors: Foster, Simon; Baxter, James
title: Automated Algebraic Reasoning for Collections and Local Variables with Lenses
date: 2020-04-01
journal: Relational and Algebraic Methods in Computer Science
DOI: 10.1007/978-3-030-43520-2_7
sha: 63cd5fec842b12cc5a46882ba93e8eebdd15d393
doc_id: 61027
cord_uid: q6ad465u

Lenses are a useful algebraic structure for giving a unifying semantics to program variables in a variety of store models. They support efficient automated proof in the Isabelle/UTP verification framework. In this paper, we expand our lens library with (1) dynamic lenses, that support mutable indexed collections, such as arrays, and (2) symmetric lenses, which allow partitioning of a state space into disjoint local and global regions to support variable scopes. From this basis, we provide an enriched program model in Isabelle/UTP for collection variables and variable blocks. For the latter, we adopt an approach first used by Back and von Wright, and derive weakest precondition and Hoare calculi. We demonstrate several examples, including verification of insertion sort.

The use of algebraic structures for derivation of verification tools using theorem provers has been shown to be a successful and flexible approach [1] [2] [3] [4] . It allows us to precisely and abstractly characterise the formal semantics of a spectrum of languages utilising different computational paradigms, including hybrid systems, concurrency, pointers, and probability. Once a suitable algebraic structure is fixed, a large array of axiomatic verification calculi can be generated, including Hoare logic [1] , differential dynamic logic [4] , separation logic [2] , and rely-guarantee calculus [3] . This approach has significant advantages over concrete intermediate verification languages (IVLs) [5, 6] , since it allows us to unify languages and verification calculi at the algebraic level, and so promotes reuse.

Nevertheless, the underlying algebras for program verification largely focus on the point-free programming operators -those that do not explicitly characterise program variables -such as sequential composition ( ) and non-deterministic choice ( ). Kleene Algebra with Tests (KAT) [3, 7] , for example, can characterise every operator of imperative while-programs, but is not sufficient to fully capture assignment, substitution, frames, and local variable blocks. Operators that manipulate the store via variables have to be defined in the model rather than the algebra [1, 3] . This technically hampers the reuse of theorems across various languages. At the same time, an algebra of state should allow efficient use of automated proof facilities, so as to support scalable verification tools.

Lenses [8] [9] [10] allow us to characterise variables as abstract algebraic objects, which can be composed and manipulated. They provide a generic foundation for verification tools that can maximise proof automation in tools like Isabelle [11, 12] . Although originating from a different intellectual stream [8] , lenses are essentially Back and von Wright's variable manipulation functions [13] . However, lenses are also equipped with several operators that allow us to compose state space query operations in sequence and in parallel, for example. Lenses are the foundation for state modelling in our verification framework, Isabelle/UTP [10, 14, 15] , which allows the use of UTP semantic models in developing program verification tools.

In previous work [10] , we showed how lenses capture a variety of store models. In this paper, we extend our basic lens model in two ways. Firstly, we develop support for indexed collections, which requires the development of dynamic lenses. Secondly, we add support for local variables, for which we harness the work of Hoffmann et al. on symmetric lenses [16] that allow us to partition the state space into global and local variable scopes. This allows us to determine whether a particular assignment can be moved outside of a block. From this foundation, we adapt Back and von Wright's block operators [13] , and prove Hoare logic theorems. Symmetric lenses allow us to unify a variety of variable block approaches, including extensible records [17] and list-based stacks [18] .

In order to illustrate these features, consider the insertion sort algorithm: It introduces two local variables, i and j , that are used to index into the array. The outer loop iterates through the list using i , and the inner loop inserts element i in the correct position into arr [0...i −1], using j to count down. To give this a semantics, we need to (1) allow assignment to the indices of a collection, and (2) extend the state space to add i and j as local variables. Our goal is to support this abstract algorithmic presentation directly in our tool, through a shallow embedding, and provide syntax-directed reasoning support.

Our approach reduces reasoning about programs to proving properties of the state space. It is therefore applicable to any language semantics with an explicit state space model, including reactive [11] and hybrid languages [4, 19] . The approach is therefore abstract, but also maximises Isabelle's proof automation.

The structure of this paper is as follows. After consideration of related work in Sect. 2, we describe how lenses give an algebraic semantics to variables in Sect. 3. In Sect. 4 we give an overview of Isabelle/UTP. In Sect. 5, we consider how a state space can be manipulated using lens operators. In Sect. 6 we describe dynamic lenses, which are needed for collections, like arrays. In Sect. 7, we describe our algebraic characterisation of symmetric lenses, and exhibit several models. In Sect. 8, we use symmetric lenses to implement local variable blocks. In Sect. 9 we use all the aforementioned results to verify insertion sort in Isabelle/UTP. Finally, in Sect. 10, we conclude.

All definitions and theorems are mechanised in Isabelle/UTP, and are often accompanied by an icon ( ) linking to the corresponding repository artefact.

Isabelle/UTP [10, 14, 15, 20] is a semantic framework for verification tools based in Hoare and He's Unifying Theories of Programming (UTP) [21] . It is broadly comparable to IVLs like Boogie [5] and Why3 [6] , but harnesses algebraic and denotational semantic techniques, for application to languages of multiple paradigms. The UTP relational program model is built as a shallow embedding [20] in Isabelle/HOL, and so we compare with similar techniques in this prover.

Simpl is an IVL developed by Schirmer in Isabelle/HOL [17, 22] . It is used in the AutoCorres verification platform [23] that was applied in the seL4 project 1 . It uses state monads augmented with exceptions to model low-level code. Our aim is to support the features and efficiency of Simpl, but using relational calculus and algebra to characterise language features abstractly so that they can be transferred between semantic models. Their work does not provide an algebraic semantics for variables, which we provide by lenses, but their comprehensive study of state space modelling techniques is a strong foundation for us [22] .

Dongol et al. [24] characterise variables algebraically using Cylindric Kleene Lattices, which extend Kleene algebra with Cylindrification to support quantification. This, in turn, allows expression of both frames and local variable blocks. Their work is largely complementary to ours, since we focus on the algebraic semantics of the variables themselves. They use ordinals as indices into an implicit state space, whereas we characterise the state space explicitly. Our use of lenses also allows us to harness type checking and proof automation in Isabelle.

Here, we review lenses [10] , which give algebraic semantics to variables. Novelties include the list-lens and a more precise presentation compared to previous work [10] . We use the notation X : V =⇒ S when X is a lens that characterises a V -shaped subregion of a state space S . For instance, in a state space A × B , we can define two lenses: fst A B : A =⇒ A × B and snd A B : B =⇒ A × B , that select the respective components. As usual [8] , we define lenses using two functions: Definition 3.1. A lens is a quadruple X (V , S , get, put), where V and S are non-empty sets called the view type and state space, respectively, and get : S → V and put : S → V → S are total functions. We often subscript get and put with the name of a lens. We define create X v put X (εs • s ∈ S ) v , which constructs an arbitrary, but fixed, state using Hilbert's choice (ε) and puts v into it. y) ), selects and updates the first element of a pair, leaving the second element unchanged. Lenses provide an intuitive and obvious way to model variables in a state space (cf. [13, 18] ), which can be queried and updated using the two functions. Intuitively, we can think of them as pointers to distinct regions of a memory store modelled by S . As previously highlighted [10, 22] , there are a variety of possible memory models, and lenses provide a uniform algebraic interface for them.

Lenses provide the starting point for the UTP relational calculus [21] , which has a model for imperative programs, including operators like sequential composition (P Q), conditional (P b Q), and assignment (x := e). Assignment is polymorphic over any lens x , provided that e matches its view type (see Sect. 4).

The behaviour of lenses is constrained by three intuitive axioms:

L1 states that a value put can be retrieved. L2 states that an earlier put is overwritten by a later put. L3 states that retrieving a value and then putting it back yields the original state. We distinguish total lenses, that obey all three axioms, from partial lenses that obey only L1 and L2. The fst and snd lenses are both total. A further example of a total lens is the total function lens:

It points to the value associated with a particular domain element x . It is useful, for instance, when the state space has type Name → Value, which associates a named variable with a value in a given universe. The get function simply applies f , and the put function updates the value associated with x . It is clear that this lens obeys all three laws. We also define a relation called independence, X Y , that characterises when two lenses view disjoint regions of the state space:

It is defined only when the state spaces are the same: S X = S Y . X and Y are independent provided applications of put commute, and each get function is unaffected by the corresponding put function. If X and Y are both total lenses, then the second and third conjuncts can be omitted. X Y means that X and Y do not interact, for example fun-lens B (i ) fun-lens B (j ), provided that i = j . Partial lenses, which do not obey L3, are motivated by partial structures, such as arrays and heaps. The cells of an array can be modelled using list lenses: 

Clearly, list-lens satisfies both L1 and L2: we can always place a value in the i th component, potentially several times, and retrieve it. However, it does not satisfy L3. When a list is too short (i ≥ #xs), list-lens(i ) returns an arbitrary value, which, if placed at i , alters the list structure and violates L3. Consequently, whilst fun-lens is a total lens, list-lens is only partial, and the same follows for data structures like partial functions. Nevertheless, as we shall see, partial lenses are sufficient to support most of the laws we need for verification calculi.

A useful class of state space is induced by records. In Isabelle/UTP, we can define a state type rec-typ [x 1 : A 1 · · · x m : A m ] for m fields, each with a given type. Technically, it is isomorphic to a product type A 1 × · · · × A m , but with named lenses for manipulating each field. The alphabet command automates the creation of these lenses, and generates theorems that x i x j for any i = j . State types can also be extended: rec-typ 2 rec-typ + [y 1 : B 1 · · · y n : B n ], which allows hierarchy. This approach is used in the IVL Impl [17] to represent local variables, and here we adopt a similar approach. The lenses are polymorphic:

where the parameter α allows application of x i to both rec-typ and extensions thereof, such as rec-typ 2 with α ∼ = A m+1 × · · · × A n . This is important, as it means that the same lens name can be used in different state spaces: x i can both have the type A i =⇒ rec-typ and A i =⇒ rec-typ 2 .

In this section, we briefly introduce the foundations of Isabelle/UTP, which is a shallow embedding of UTP [21] in Isabelle/HOL. UTP is based on a variant of Tarski's relational calculus [25] where each relation is "alphabetised", meaning it is parameterised by the set of variables to which it can refer. In Isabelle/UTP, we instead opt to have relations parameterised by their state space type S , and variables are then lenses viewing this type. We can therefore use the Isabelle type system to ensure well-formedness: only relations and predicates with compatible alphabets can be composed using the Boolean and relational connectives.

Expressions are total functions: [V , S ]expr (S → V ), for some state space S and type V . Operators can be pointwise lifted and applied to them, for example, if e, f : [N, S ]expr, then e +f denotes λ s : S • e s +f s. If x and y are lenses, then we can use them in expressions: x + y denotes λ s : S • get x s + get y s. We can determine whether e depends on part of the state using the unrestriction [10] :

Lens x is unrestricted in e, written x e, when updating its value using put has no effect on the valuation of e. This can occur, for example, when x is a variable that e does not refer to. Unrestriction distributes through lifted functions [10] . Substitutions between two states spaces are modelled with functions, σ : S 1 → S 2 . A substitution can be updated using σ(x → e). A heterogeneous substitution can be constructed using x 1 → e 1 , · · · , x n → e n , when x i : A i =⇒ S 2 and e i : [A i , S 1 ]expr, which is a set of simultaneous updates. A homogeneous substitution, where S 1 = S 2 , can be constructed similarly but using square brackets: [x → e, · · · ]. The difference between these two is that the former gives arbitrary values to unassigned variables, whereas the latter copies the original values. Substitutions can also be composed function-wise, σ • ρ, which corresponds to applications of the updates in ρ followed by those in σ.

We can apply a substitution to an expression using σ † e e • σ, which likewise composes the substitution and expression functions. Although this may seem redundant, it is useful to distinguish a separate operator to enable bespoke rewrite laws in Isabelle. Then, we can obtain the traditional substitution oper-

Substitutions then obey a number of useful laws:

Theorem 4.2. If x and y are partial lenses, then the following laws hold:

Substitution updates commute when made to independent lenses (1), and can cancel earlier ones (2) . Substitutions can be composed, and (3) shows how to pull out a variable update to the left-most substitution. These laws can be used to

, when x y. Substitution application distributes through functions in the obvious way, and can be applied to variable expressions (4) . If x is unrestricted in an expression, then any assignment to this variable can be dropped (5) .

We define predicates,

pred, and the usual operators over them. Predicates and relations are ordered by refinement ( ). We import theorems for structures like complete lattices, quantales, and Kleene algebras [2, 3, 10] . With substitutions, it is easy to define a generalised assignment operator, in the style of Back and von Wright [13] : σ , which lifts a substitution to a relation in the obvious way. This satisfies a useful law, σ ρ = ρ • σ , which allows us to combine sequential assignments. Assignments can then be constructed with x := e [x → e] , and combining with non-deterministic choice ( ) we define non-deterministic assignment:

These definitions satisfy the laws of programming [26] .

Here, we show how to manipulate state spaces, and coerce variables and expressions between them. We use two additional relations, that are defined using get and put [10] : (1) X Y : the view of lens X is contained within the view of Y ; (2) X ≈ Y : the views of X and Y are isomorphic. These are both heterogeneous operators that can relate lenses with different view types. Relation forms a preorder and ≈ is an equivalence relation. Ordering is needed because lenses can characterise both variables and sets thereof. We compose lenses, thus combining their respective views, using the pairing operator:

Lens pairing combines two independent lenses with the same state space, creating a lens whose view type is V X × V Y . The get function pairs the results of the get functions for X and Y , while its put function puts each element using the respective put. Using this, a set of variables, {x , y, z } can be characterised by a lens, for example, by the summation x ⊕ y ⊕ z . Moreover, we have it that X X ⊕ Y , since X ⊕ Y views more of the state space than X . We define two basic total lenses: 1 S (S , S , λ s • s, λ s v • v ) whose view and state space are identical, and 0 S ({∅}, S , λ s • ∅, λ s v • s), whose view type is unitary. Intuitively, 1 characterises the entirety of S , and 0 characterises none of it, and cannot distinguish any states. Consequently, we have 0 X and X 1 , since these are the least and most distinguishing lenses, respectively.

For variable blocks, we need expansion and contraction of the state space, for both lenses and expressions. For lenses, we define the composition and quotient: Definition 5.2 (Lens Composition and Quotient).

Y has been previously defined [8] . It selects a subregion V 1 , characterised by X : V 1 =⇒ V 2 , of a larger region V 2 , characterised by Y : V 2 =⇒ S . Intuitively, Y denotes a sub-space of S , X is a variable of this sub-space, and so X ; Y Y . We sometimes write obj:attr for the composition attr ; obj .

We believe the quotient operator, X /Y is novel 2 . Provided that X : V 1 =⇒ S is constructed by composition of Y : V 2 =⇒ S and Z : V 1 =⇒ V 2 , we have it that X /Y = Z . The get function first creates an arbitrary state and populates the V 2 region with the incoming state. It then uses the get X function to obtain the V 1 element. The assumption is that all the information needed to construct a V 1 can be obtained from V 2 . The put function creates an S element, uses put X to update this with v : V 1 , and finally applies get Y to obtain a V 2 element. Again, the assumption is that put X will only manipulate data within V 1 .

Lens quotient gives rise to some useful, and intuitive, properties.

The first identity gives the intuition of quotient: it removes the second element of a composition. The second identity shows that if we remove a lens from itself, then only a residual 1 remains. The third identity shows that removal of 1 has no effect, because of course X ; 1 = X .

In addition, we need to expand and contract the state space of expressions: Here, X is a lens that describes how S 1 is embedded into a larger space S 2 . The first operator, e ↑ X , extends the state space of e to be S 2 , and the second, f ↓ X , restricts it to be S 1 . These operators coerce an expression to have a different type, for use in a context with a different state space. They satisfy several theorems.

.

Both extension and restriction distribute through function application in the obvious way. Extension of a lens expression entails a lens composition, and restriction entails a lens quotient. If we extend an expression's state space, e ↑ A, then the resulting expression does not depend on a lens B that is independent of A. The reason is that the original state space of e is characterised by A. Finally, we have it that restriction is the inverse of extension. The converse theorem does not hold, because restricting a state space may result in a loss of information.

We can define e e ↑ fst, e e ↓ fst, and e a ↑ snd, that characterise relational preconditions and postconditions. Specifically, e lifts an expression on S to one on S × S , thus turning a predicate into a relation. We can characterise initial and final variables, x and x , in the style of notations like Z. We can also define weakest preconditions, P wp b (P b ) , and also the Hoare triple,

These definitions admit, as theorems, the usual laws [27, 28] . For example, we have the assignment law,

for any lens x , and the more general { σ † p } σ { p }.

In this section we give semantics to the notation x [i ], which refers to the i th element of a collection x . We model x with a lens that points to a collection, such as a list, and i with an index expression. The generality of the lens axioms means that we can define x [i ] itself to be a type of lens, which we call the collection lens. Consequently, we can manipulate it like any other lens, employing the theorems of Sect. 4. In order to define this, we first need to define dynamic lenses: Definition 6.1. We fix sets A and B that denote elements and collections, and a set I of indices. We assume a family of I -indexed lenses F : I → (A =⇒ B ) and an expression e : B → I . A dynamic lens is defined as follows:

Intuitively, a dynamic lens points to the eth element of the indexed lens F . Since e is an expression, it can change value, and consequently the current index depends on the state space. The get and put function both instantiate the indexed lens with e applied to the current state, and then apply its respective get and put function. From this definition, we can prove the following closure theorem: Theorem 6.2. We assume that, for all i : I , e does not refer to F i, that is (F i) e, and F i is a partial or total lens. We can then show that dyn-lens F e is a partial or total lens, respectively.

The intuition is that F i must satisfy the lens axioms, for all indexes, and the index expression e should not itself refer to the F i, to avoid self references. From this definition, we can now define collection lenses: x [e] dyn-lens (λ i :

The collection lens, x [e], is a dynamic lens where the underlying indexed lens F is applied after selection of the collection location in the lens x . It is clear that Theorem 6.2 can be applied here too, provided that x is also a total lens. The intuition of the collection lens is perhaps clearer if we consider a concrete example where F = fun-lens. In this case, we can prove the following identity: In Isabelle/UTP, we make F an overloaded polymorphic constant that associates a suitable indexed lens to a collection type. In many situations, x [e] is a partial lens, since it is only meaningful when x is a collection where the key e is defined. For example, the assignment (arr [j − 1], arr [j ]) := (arr [j ], arr [j − 1]) in Example 1.1 is meaningful only when j < #arr . Thus, when verifying programs with collection lenses, it is necessary to guard them with definedness predicates.

Symmetric lenses [16] stand in contrast to the lenses that were introduced in Sect. 3, which are "asymmetric" because, once a view has been extracted from a source, it is not possible to reconstruct the source from the view alone [16] . Symmetric lenses are effectively lenses of type V × C =⇒ S , where C is the "complement" of V with respect to S -the remainder of S once V is removed. In general, it is not possible to compute the complement of an asymmetric lens. Symmetric lenses thus capture the notion of partitioning the state into disjoint regions. These regions are represented by two lenses, which we refer to as the view and the coview, and for a given symmetric lens X , we write V X and C X to represent them. Such a partitioning of the state space is fundamental to framing of certain variables, and allows us to distinguish the global and local store.

To characterise symmetric lenses, we must capture both the disjointness of the view and coview, and the fact that, taken together, they cover the state space. Coverage is captured by first combining the view and coview into a pairing V X ⊕ C X , and requiring that this covers the state space. Such a definition is provided for by the concept of bijective lenses, defined below. For total bijective lenses, we require that getting the view of s and putting it into s replaces the whole of s with s . For a partial lens, get may return an incorrect value for states outside its domain, so a partial bijective lens is characterised by put s v = put s v . This captures the property that put replaces the state space, without constraining get. A bijective lens fulfils all the axioms of a partial or total lens, but it is sufficient to require L1, so the overall definition of a bijective lens is as shown above. We can now define symmetric lenses:

(V, C) over a state space S is a pair of (partial) total lenses, V : V 1 =⇒ S and C : V 2 =⇒ S such that (1) V C, and (2) V ⊕C is a (partial) bijective lens. We denote the set of symmetric lenses between V 1 × V 2 and S with the notation

As an example of a symmetric lens, consider X (fst A , snd B ) . These lenses are clearly independent, and fst A ⊕ snd B provides a view of the entire product, so it is a bijective lens. Thus, X is a (total) symmetric lens.

A more interesting example is the list symmetric lens, the view and coview of which are the head and tail of a list. Formally, they are the head lens, hd A : , λ xs v • hd xs v ) . It gets the tail of the list, and puts xs as the tail of the new list, preserving the old head. These lenses are independent, since they operate on different parts of a list. The head lens, as an instance of the list lens, is a partial lens, since it is not defined for an empty list. The list symmetric lens is thus an example of a partial symmetric lens, since putting a list head and tail replaces the whole list. We note that the tail lens has the same view and source types. This is an important property for allowing variable blocks based on such symmetric lenses to be recursed on [18] , as we discuss in Sect. 8.

Another symmetric lens is induced by record state spaces, each of which induces two regions: the base region, which consists of the defined fields (x 0 · · · x m ), and the extension region, with any additional fields (y 0 · · · y n ). These can be characterised by base : rec-typ =⇒ [α]rec-typ-ext and more : α =⇒ [α]rec-typ-ext, where base more and base ⊕ more is a bijective lens. Consequently, for a record we define all (base, more), which forms a total symmetric lens. Moreover, we have it that x i base, for 0 ≤ i ≤ m, and y j more, for 0 ≤ j ≤ n.

The polymorphic nature of a record lens means that type coercions can be handled easily, as the following theorem shows.

Composition and quotient using the base lens corresponds to moving it into and out of an extended state space. Since x i : V i =⇒ [α]rec-typ-ext is polymorphic, such a coercion yields the same lens but with a different type. These laws are important for when moving a global variable into a local scope in Sect. 8.

Having defined symmetric lenses, and demonstrated several models, we now use these to characterise local variable blocks. The basic idea is to implement operators analogous to begin and end from Back and von Wright [13, § 5.6] , that grow and shrink the state space with additional variables.

Here, however, we fix a symmetric lens X : [S 2 , C ] ⇐⇒ [S 1 ] to give a concrete semantics to scope expansion and contraction. Intuitively, S 2 is the global state space, S 1 extends S 2 with local variables, and C is the complement of S 2 wrt. S 1 . Then we have it that V X characterises the global state region of S 1 , and C X the local state region. The symmetric lens allows us to distinguish global and local variables, so that we can determine whether an assignment can be moved outside a block or not. Unlike [13] , where types are implicit, we have to explicitly handle type coercion when a variable and expression moves between state spaces.

We give the following program that swaps two variables as a running example: It creates a third variable, z , and then uses this as a temporary store in which to place the value of y. We show how this can be modelled and verified in Isabelle/UTP, with the aim of supporting the larger insertion sort example in Sect. 9. We first define substitutions that extend and contract the state space.

.

Here, ext X : S 2 → S 1 and con X : S 1 → S 2 are heterogeneous substitutions. Extension assigns the original state (v : S 2 ) to the view lens (V X ), and assigns an arbitrary but fixed element of C to the coview lens. Effectively this extends the state space, retaining the values for the global variables, and assigning an arbitrary value to the local ones. Contraction, conversely, assigns the view lens to the entire state lens, leading to the loss of the local state. Extension and contraction satisfy the theorem below:

Specifically, if we extend a state space and then contract it, we always get the original state space back. The converse of this law does not hold since contracting a state space, of course, loses the local state stored in the coview. Moreover, the law only follows for total symmetric lenses since extending and then contracting using a partial lens can alter the state. It is now straightforward to define relations that open and close a block using the substitutions:

Here, open X : [S 2 , S 1 ]rel first extends the state space and then nondeterministically assigns a value to the coview, replacing the arbitrary but fixed value. Also, close X simply contracts the state space. We prove a useful law:

Theorem 8.5. Any symmetric lens X satisfies open X close X = I I.

Aside from being an important property of variable blocks, this law allows us to introduce a local variable block at any point in a program, which can facilitate step-wise refinement. We now prove three algebraic laws for variable blocks and assignments, which are adapted from [13, page 102].

Theorem 8.6 (Variable Block Laws).

y := v close X = close X when y C X (7)

x :

An assignment to a global variable x can be pushed into a variable block (6) . We have to coerce both the variable and the assigned expression using lens composition and the state space extension operators, respectively. An assignment to a local variable y C X at the end of a block is lost (7) . An assignment to a global variable in a block can be moved past the end (8) . Again, it is necessary to coerce the variable and expression, using lens quotient and state space restriction, this time to contract the state space. Moreover, this law only applies when the expression does not refer to local variables, given by the condition C X v . These latter two laws show how the symmetric lens allows us to distinguish local and global variables. We can also derive a Hoare logic law for variable blocks:

The intuition is that p and q must be augmented with additional variables in the enlarged state space, and references to global variables must be type cast. We can now model the algorithm in Example 8.1. First, we need to create global and local state spaces and a suitable symmetric lens. The global state space can be described by global [x : int, y : int], as explained in Sect. 3. This gives rise to base : global =⇒ [α]global-ext and more : α =⇒ [α]global-ext, which together form a symmetric lens all . Moreover, the local state can be described by the record local global + [z : int], and so we specialise global 's base lens, base, to have type global =⇒ local. In Isabelle/UTP, local can be generated on-the-fly in a record block, to support the syntax given in Example 8.1. This approach, using extensible records for variable blocks, is used in Simpl [17] .

An implementation is shown in Fig. 1 , along with several theorems. We construct global using the alphabet command, and then define swap, with a near identical representation to Example 8.1. The decorations &z and U(·) are hints to parser with no semantic content. The machinery for creating local and instantiating the symmetric lens is hidden behind the var construct, though we have to explicitly state that we are using the all symmetric lens from the global state space. We then prove three theorems. The first one calculates a weakest precondition, the second a Hoare triple, and the final one shows that swap can actually be replaced by a simultaneous assignment, assuming this is supported.

While the use of records in blocks provides strong typing, the fact that the all symmetric lens changes the type of the state space means it cannot be used in recursive functions. This was previously observed by Back and Preoteasa [18] . To handle recursion, the symmetric lens must describe a global state with the same type as the overall state space (which includes both global and local). As mentioned previously, (hd A , tl A ) is such a lens, and so is its converse (tl A , hd A ). This symmetric lens creates variable blocks that push an arbitrary value onto the start of a list, creating a stack semantics.

The fact that the list symmetric lens forms a partial lens creates the need for domain checks when variables in the list are accessed. Such checks can be avoided by using a state space with a function from natural numbers to values instead of a list. We define head and tail lenses on such a state space as follows:

These head and tail lenses are total lenses, since they are defined on a total function. We can thus define a total symmetric lens using them in a similar way to the list symmetric lens. These lenses can also be lifted to a state space with additional global state in a similar way to the list symmetric lens. We have mechanised these definitions in Isabelle/UTP and proved the resultant lens is indeed a total symmetric lens. We have also proved properties for a swap function using this symmetric lens as we did for the record symmetric lens. This shows the flexibility of our lens-based approach to local variables: list or function lenses can be used where support for recursion is required, while record lenses can be used where the added structure of Isabelle's type system is desired.

Here, we show how we have used the collected results of the previous sections to verify the insertion sort algorithm in Isabelle/UTP. We model the algorithm using both collection lenses and symmetric lens variable blocks, as shown in Fig. 2 . In order to ease verification, we split the algorithm into two definitions: one for the inner loop (insert-elem), and one for the outer loop (insertion-sort). Both are specified as functions that take the list to be sorted, xs, as a parameter. The syntax of the program broadly follows that given in Example 1.1. The only significant deviation is that we have manually constructed a symmetric lens lv that uses an explicit local state space. This is so that i and j can be referred to as global names in the Isabelle theory, to enable description of the invariants. The outer program itself operates on a state space where only arr is present, and the other variables are introduced by open and close.

As usual [1] , our loop construct supports invariant annotation, using the invr keyword. The invariant of the inner loop (I xs) is not shown due to its complexity. The outer loop invariant states that (1) 0 < i ≤ #arr , it is within the array bounds; (2) the array in the range 0 · · · i −1 is sorted; and (3) The program is verified using Hoare logic as shown in Fig. 3 . The proof is quite long, due to the number of proof obligations, and some manual effort is required. This seems mainly due to missing lemmas, and so in future the proof should be more automated (cf. [12] ). Nevertheless, for now we omit details of the proof steps. The first Hoare triple demonstrates that the inner loop preserves the invariant of the outer loop. The outer loop shows that, when provided with a non-empty list a sorted permutation of xs is returned in arr .

In this paper we have shown how lenses support modelling and verification of algorithms in the Isabelle/UTP tool [11] . We introduced dynamic lenses, that allow us to handle collections, and symmetric lenses, that allow partitioning of the state space into disjoint regions. Collection lenses allow us to generically characterise a variety of different indexed collection types in Isabelle/UTP, including arrays and maps. Symmetric lenses [16] allow us to characterise state partitioning, and we have used them here to distinguish local and global variables scopes. Due to typed nature of our state spaces, coercions are necessary when moving between scopes, which we can also handle using lenses. Our conclusion is that algebraic characterisation in this way is both flexible and practical, as our verification of insertion sort demonstrates. Moreover, since our characterisation sits at the state space level, our results are applicable to paradigms beyond imperative programming, such as reactive [11] and hybrid programming [4, 19] .

In future work, we will explore symmetric lenses and their properties further. We note that there are several different models for symmetric lenses, including extensible records, lists, and total functions, each with unique advantages. We can use extensible records to support variables with native type checking, but they cannot support recursion, as for example required by quicksort, due to a priori bounding of the state space. In contrast, list and function symmetric lenses overcome this limitation, but require a fixed element type. Our mechanisation thus allows us chose the best model for a particular circumstance. In the future, we will perform a detailed comparison of the different models.

Building program construction and verification tools from algebraic principles

A program construction and verification tool for separation logic

Modal Kleene algebra applied to program correctness

Verifying hybrid systems with modal Kleene algebra

Boogie: a modular reusable verifier for object-oriented programs

Why3-where programs meet provers

Kleene algebra with tests

Combinators for bidirectional tree transformations: a linguistic approach to the view-update problem

Quotient lenses

Unifying heterogeneous state-spaces with lenses

Unifying theories of reactive design contracts. Theor

Using Isabelle/UTP for the verification of sorting algorithms

Refinement Calculus: A Systematic Introduction

Isabelle/UTP: a mechanised theory engineering framework

Isabelle/UTP: mechanised theory engineering for unifying theories of programming

Symmetric lenses

The Verisoft approach to systems verification

An algebraic treatment of procedure refinement to support mechanical verification

Hybrid relations in Isabelle/UTP

Unifying theories in Isabelle/HOL

Unifying Theories of Programming

State spaces -the locale way

Don't sweat the small stuff: formal verification of C code without the pain

Cylindric Kleene lattices for program construction

On the calculus of relations

The laws of programming

An axiomatic basis for computer programming

Guarded commands, nondeterminacy and formal derivation of programs

Acknowledgements. This work is funded by the EPSRC projects CyPhyAssure (CyPhyAssure Project: https://www.cs.york.ac.uk/circus/CyPhyAssure/.) (Grant EP/S001190/1) and RoboTest (Grant EP/R025479/1).