University of Surrey

Test tubes in the lab Research in the ATI Dance Research

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.

Cylindric Kleene Lattices for Program Construction.pdf - Accepted version Manuscript

Download (404kB) | Preview


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 :
Hayes, Ian
Meinicke, Larissa
Struth, Georg
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

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800