Unifying heterogeneous state-spaces with lenses.

Most verification approaches embed a model of program state into their semantic treatment. Though a variety of heterogeneous state- space models exists, they all possess common theoretical properties one would like to abstractly capture, such as the laws of programming. In this paper, we propose lenses as a universal state-space modelling solution. Lenses provide an abstract interface for manipulating data types through spatially-separated views. We dene a lens algebra that allow their composition and comparison. We show how this algebra can be used to model variables and alphabets in Hoare and He's Unifying Theories of Programming. The combination of lenses and relational algebra gives rise to a model for UTP in which its fundamental laws can be verified. Moreover, we illustrate how they can be used to model more state complex notions such as memory stores and parallel states. We provide a mechanisation in Isabelle/HOL that validates our theory, and facilitates its use in program verification.