Unifying heterogeneous state-spaces with lenses.

Simon Foster, Frank Zeyda, Jim Woodcock

    Research output: Contribution to conferencePaperResearchpeer-review

    18 Downloads (Pure)

    Abstract

    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

    Conference

    Conference13th ICTAC International Colloquium on Theoretical Aspects of Computing
    CountryTaiwan, Province of China
    CityTaipei
    Period24/10/1630/10/16

    Fingerprint

    lenses
    algebra
    programming
    mechanization
    alphabets
    semantics

    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.
    Foster, Simon ; Zeyda, Frank ; Woodcock, Jim. / Unifying heterogeneous state-spaces with lenses. Paper presented at 13th ICTAC International Colloquium on Theoretical Aspects of Computing, Taipei, Taiwan, Province of China.
    @conference{4e902104481946e1be6b15f4783d6b7b,
    title = "Unifying heterogeneous state-spaces with lenses.",
    abstract = "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.",
    author = "Simon Foster and Frank Zeyda and Jim Woodcock",
    year = "2016",
    month = "10",
    day = "30",
    language = "English",
    note = "13th ICTAC International Colloquium on Theoretical Aspects of Computing ; Conference date: 24-10-2016 Through 30-10-2016",

    }

    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, 24/10/16 - 30/10/16, .

    Unifying heterogeneous state-spaces with lenses. / Foster, Simon; Zeyda, Frank; Woodcock, Jim.

    2016. Paper presented at 13th ICTAC International Colloquium on Theoretical Aspects of Computing, Taipei, Taiwan, Province of China.

    Research output: Contribution to conferencePaperResearchpeer-review

    TY - CONF

    T1 - Unifying heterogeneous state-spaces with lenses.

    AU - Foster, Simon

    AU - Zeyda, Frank

    AU - Woodcock, Jim

    PY - 2016/10/30

    Y1 - 2016/10/30

    N2 - 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.

    AB - 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.

    M3 - Paper

    ER -

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