Cylindric Kleene Lattices for Program Construction
Dongol, Brijesh, Hayes, Ian, Meinicke, Larissa and Struth, Georg (2019) Cylindric Kleene Lattices for Program Construction In: 13th International Conference on Mathematics of Program Construction, 07-09 Oct 2019, Porto, Portugal.
|
Text
Cylindric Kleene Lattices for Program Construction.pdf - Accepted version Manuscript Download (404kB) | Preview |
Abstract
Cylindric algebras have been developed as an algebraisation of equational first order logic. We adapt them to cylindric Kleene lattices and their variants and present relational and relational fault models for these. This allows us to encode frames and local variable blocks, and to derive Morgan's refinement calculus as well as an algebraic Hoare logic for while programs with assignment laws. Our approach thus opens the door for algebraic calculations with program and logical variables instead of domain-specific reasoning over concrete models of the program store. A refinement proof for a small program is presented as an example.
Item Type: | Conference or Workshop Item (Conference Paper) | |||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Divisions : | Faculty of Engineering and Physical Sciences > Computer Science | |||||||||||||||
Authors : |
|
|||||||||||||||
Date : | 7 October 2019 | |||||||||||||||
Funders : | Engineering and Physical Sciences Research Council (EPSRC) | |||||||||||||||
Copyright Disclaimer : | © 2019 Springer-Verlag Berlin Heidelberg | |||||||||||||||
Related URLs : | ||||||||||||||||
Depositing User : | Clive Harris | |||||||||||||||
Date Deposited : | 19 Aug 2019 12:54 | |||||||||||||||
Last Modified : | 07 Oct 2019 02:08 | |||||||||||||||
URI: | http://epubs.surrey.ac.uk/id/eprint/852438 |
Actions (login required)
![]() |
View Item |
Downloads
Downloads per month over past year