
Algebra
of
Monotonic
Boolean
Transformers
Title: 
Algebra of Monotonic Boolean Transformers 
Author:

Viorel Preoteasa (viorel /dot/ preoteasa /at/ aalto /dot/ fi)

Submission date: 
20110922 
Abstract: 
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 formalize here an algebra which can be used to model total correctness, refinement, demonic and angelic choice. The basic model of this algebra are monotonic Boolean transformers (monotonic functions from a Boolean algebra to itself). 
BibTeX: 
@article{MonoBoolTranAlgebraAFP,
author = {Viorel Preoteasa},
title = {Algebra of Monotonic Boolean Transformers},
journal = {Archive of Formal Proofs},
month = sep,
year = 2011,
note = {\url{https://isaafp.org/entries/MonoBoolTranAlgebra.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
LatticeProperties 
Used by: 
Correctness_Algebras 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

