Unifying heterogeneous state-spaces with lenses

Simon Foster*, Frank Zeyda, Jim Woodcock

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 capture abstractly,such as the common algebraic 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 define a lens algebra that enables their composition and comparison,and apply it to formally model variables and alphabets in Hoare and He’s Unifying Theories of Programming (UTP). 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 lenses can be used to model more complex state 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.

Original languageEnglish
Title of host publicationTheoretical Aspects of Computing - ICTAC 2016, 13th International Colloquium, Proceedings
EditorsFarn Wang, Augusto Sampaio
Number of pages20
ISBN (Electronic)978-3-319-46750-4
ISBN (Print)978-3-319-46749-8
Publication statusPublished - 24 Oct 2016
Event13th International Colloquium on Theoretical Aspects of Computing, ICTAC 2016 - Taipei, Taiwan
Duration: 24 Oct 201631 Oct 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9965 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference13th International Colloquium on Theoretical Aspects of Computing, ICTAC 2016

Cite this