Unifying heterogeneous state-spaces with lenses.

Simon Foster, Frank Zeyda, Jim Woodcock

    Research output: Contribution to conferencePaperpeer-review

    100 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
    Country/TerritoryTaiwan, Province of China


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

    Cite this