By the same authors

Unifying heterogeneous state-spaces with lenses

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

Full text download(s)

Links

Published copy (DOI)

Author(s)

Department/unit(s)

Publication details

Title of host publicationTheoretical Aspects of Computing - ICTAC 2016, 13th International Colloquium, Proceedings
DateAccepted/In press - 1 Jul 2016
DatePublished (current) - 24 Oct 2016
Pages295-314
Number of pages20
PublisherSpringer Verlag
EditorsFarn Wang, Augusto Sampaio
Original languageEnglish
ISBN (Electronic)978-3-319-46750-4
ISBN (Print)978-3-319-46749-8

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

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

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations