TY - GEN

T1 - Unifying heterogeneous state-spaces with lenses

AU - Foster, Simon

AU - Zeyda, Frank

AU - Woodcock, Jim

PY - 2016/10/24

Y1 - 2016/10/24

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

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

UR - http://www.scopus.com/inward/record.url?scp=84996486787&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-46750-4_17

DO - 10.1007/978-3-319-46750-4_17

M3 - Conference contribution

AN - SCOPUS:84996486787

SN - 978-3-319-46749-8

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 295

EP - 314

BT - Theoretical Aspects of Computing - ICTAC 2016, 13th International Colloquium, Proceedings

A2 - Wang, Farn

A2 - Sampaio, Augusto

PB - Springer

T2 - 13th International Colloquium on Theoretical Aspects of Computing, ICTAC 2016

Y2 - 24 October 2016 through 31 October 2016

ER -