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

BSD License### Topics

### Theories of 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