Unifying heterogeneous state-spaces with lenses.

Simon Foster, Frank Zeyda, Jim Woodcock

    Research output: Contribution to conferencePaper

    79 Downloads (Pure)


    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.
    Original languageEnglish
    Publication statusPublished - 30 Oct 2016
    Event13th ICTAC International Colloquium on Theoretical Aspects of Computing - Taipei, Taiwan, Province of China
    Duration: 24 Oct 201630 Oct 2016


    Conference13th ICTAC International Colloquium on Theoretical Aspects of Computing
    CountryTaiwan, Province of China

    Fingerprint Dive into the research topics of 'Unifying heterogeneous state-spaces with lenses.'. Together they form a unique fingerprint.

  • Cite this

    Foster, S., Zeyda, F., & Woodcock, J. (2016). Unifying heterogeneous state-spaces with lenses.. Paper presented at 13th ICTAC International Colloquium on Theoretical Aspects of Computing, Taipei, Taiwan, Province of China.