Refinement algebra with dual operator

Algebras of imperative programming languages have been successful in reasoning about programs. In general an algebra of programs is an algebraic structure with programs as elements and with program compositions (sequential composition, choice, skip) as algebra operations. Various versions of these a...

Full description

Saved in:
Bibliographic Details
Published in:Science of computer programming 2014-10, Vol.92, p.179-210
Main Author: Preoteasa, Viorel
Format: Article
Language:English
Subjects:
Algebra of programming
Data refinement
Hoare logic
Refinement algebra
Refinement calculus
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Algebras of imperative programming languages have been successful in reasoning about programs. In general an algebra of programs is an algebraic structure with programs as elements and with program compositions (sequential composition, choice, skip) as algebra operations. Various versions of these algebras were introduced to model partial correctness, total correctness, refinement, demonic choice, and other aspects. We introduce here an algebra which can be used to model total correctness, refinement, demonic and angelic choice. The basic model of our algebra are monotonic Boolean transformers (monotonic functions from a Boolean algebra to itself). •We introduce an extension of the general refinement algebra with a dual operator.•We introduce assertions and assumptions with simpler definitions than before.•We defined the termination and enabledness operators in our algebra.•We prove data refinement and Hoare rules, and we used them for an example program.•All results are formalized in the Isabelle theorem prover.
ISSN:0167-6423
1872-7964
DOI:10.1016/j.scico.2013.07.002