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.

[img]
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 :
NameEmailORCID
Dongol, Brijeshb.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 :
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 View Item

Downloads

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