Algebra of Monotonic Boolean Transformers
- 296 Downloads
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).
KeywordsBoolean Algebra Sequential Composition Dual Operator Total Correctness Monotonic Transformer
Unable to display preview. Download preview PDF.
- 1.Back, R.-J.: On the correctness of refinement in program development. PhD thesis, Department of Computer Science, University of Helsinki (1978)Google Scholar
- 17.Preoteasa, V.: Program Variables – The Core of Mechanical Reasoning about Imperative Programs. PhD thesis, Turku Centre for Computer Science (November 2006)Google Scholar