### Abstract

We study models of state-based non-deterministic sequential computations and describe them using algebras. We propose algebras that describe iteration for strict and non-strict computations. They unify computation models which differ in the fixpoints used to represent iteration. We propose algebras that describe the infinite executions of a computation. They lead to a unified approximation order and results that connect fixpoints in the approximation and refinement orders. This unifies the semantics of recursion for a range of computation models. We propose algebras that describe preconditions and the effect of while-programs under postconditions. They unify correctness statements in two dimensions: one statement applies in various computation models to various correctness claims.

### License

BSD License

### Topics

- Computer science/Programming languages/Logics

### Session Correctness_Algebras

- Base
- Omega_Algebras
- Capped_Omega_Algebras
- General_Refinement_Algebras
- Lattice_Ordered_Semirings
- Boolean_Semirings
- Binary_Iterings
- Binary_Iterings_Strict
- Binary_Iterings_Nonstrict
- Tests
- Test_Iterings
- N_Semirings
- N_Semirings_Boolean
- N_Semirings_Modal
- Approximation
- Recursion_Strict
- N_Algebras
- Recursion
- N_Omega_Algebras
- N_Omega_Binary_Iterings
- N_Relation_Algebras
- Domain
- Domain_Iterings
- Domain_Recursion
- Extended_Designs
- Relative_Domain
- Relative_Modal
- Complete_Tests
- Complete_Domain
- Preconditions
- Hoare
- Hoare_Modal
- Pre_Post
- Pre_Post_Modal
- Monotonic_Boolean_Transformers
- Monotonic_Boolean_Transformers_Instances

### Depends on

- Algebra of Monotonic Boolean Transformers
- Stone-Kleene Relation Algebras
- A Hierarchy of Algebras for Boolean Subsets

## Cite

×

Correctness_Algebras-AFP

    @article{Correctness_Algebras-AFP,
      author  = {Walter Guttmann},
      title   = {Algebras for Iteration, Infinite Executions and Correctness of Sequential Computations},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Correctness_Algebras.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
- Oct 20, 2021 : Isabelle2021