### Abstract

These mathematical components formalise predicate transformer semantics for programs, yet currently only for partial correctness and in the absence of faults. A first part for isotone (or monotone), Sup-preserving and Inf-preserving transformers follows Back and von Wright's approach, with additional emphasis on the quantalic structure of algebras of transformers. The second part develops Sup-preserving and Inf-preserving predicate transformers from the powerset monad, via its Kleisli category and Eilenberg-Moore algebras, with emphasis on adjunctions and dualities, as well as isomorphisms between relations, state transformers and predicate transformers.

### License

BSD License

### Topics

- Mathematics/Algebra
- Computer science/Semantics and reasoning

### Session Transformer_Semantics

- Isotone_Transformers
- Sup_Inf_Preserving_Transformers
- Powerset_Monad
- Kleisli_Transformers
- Kleisli_Quantaloid
- Kleisli_Quantale

### Depends on

- Properties of Orderings and Lattices
- Quantales

### Used by

- Verification Components for Hybrid Systems

### Auto-related entries

- Kleene Algebras with Domain
- Semantics and Data Refinement of Invariant Based Programs

## Cite

×

Transformer_Semantics-AFP

    @article{Transformer_Semantics-AFP,
      author  = {Georg Struth},
      title   = {Transformer Semantics},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Transformer_Semantics.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
- Dec 19, 2018 : Isabelle2018