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.

Preview

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 :	Name Email ORCID Dongol, Brijesh b.dongol@surrey.ac.uk 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 :	Organisation
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