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 -