### 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).

### License

BSD License

### Topics

- Computer science/Programming languages/Logics

### Session MonoBoolTranAlgebra

- Mono_Bool_Tran
- Mono_Bool_Tran_Algebra
- Assertion_Algebra
- Statements

### Depends on

- Lattice Properties

### Used by

- Algebras for Iteration, Infinite Executions and Correctness of Sequential Computations

### Auto-related entries

- Conservation of CSP Noninterference Security under Concurrent Composition
- Conservation of CSP Noninterference Security under Sequential Composition
- Putting the `K' into Bird’s derivation of Knuth-Morris-Pratt string matching
- Signature-Based Gröbner Basis Algorithms
- Imperative Insertion Sort

## Cite

×

MonoBoolTranAlgebra-AFP

    @article{MonoBoolTranAlgebra-AFP,
      author  = {Viorel Preoteasa},
      title   = {Algebra of Monotonic Boolean Transformers},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2011},
      note    = {\url{https://isa-afp.org/entries/MonoBoolTranAlgebra.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Sep 27, 2011 : Isabelle2011