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.
CITATION STYLE
Dongol, B., Hayes, I., Meinicke, L., & Struth, G. (2019). Cylindric Kleene Lattices for Program Construction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11825 LNCS, pp. 197–225). Springer. https://doi.org/10.1007/978-3-030-33636-3_8
Mendeley helps you to discover research relevant for your work.