Algebras for correctness of sequential computations

• We uniformly cover multirelational, matrix-based and relational computation models.
• Our models support angelic and demonic non-determinism.
• Our precondition operation instantiates to modal diamond and modal box operators.
• We verify all results in Isabelle, heavily using its automated theorem provers.
• We integrate our theories with the existing Isabelle theory of monotonic Boolean transformers.

Previous work gives algebras for uniformly describing correctness statements and calculi in various relational and matrix-based computation models. These models support a single kind of non-determinism, which is either angelic, demonic or erratic with respect to the infinite executions of a computation. Other models, notably isotone predicate transformers or up-closed multirelations, offer both angelic and demonic choice with respect to finite executions. We propose algebras for a theory of correctness which covers these multirelational models in addition to relational and matrix-based models. Existing algebraic descriptions, in particular general refinement algebras and monotonic Boolean transformers, are instances of our theory. Our new description includes a precondition operation that instantiates to both modal diamond and modal box operators. We verify all results in Isabelle, heavily using its automated theorem provers. We integrate our theories with the Isabelle theory of monotonic Boolean transformers making our results applicable to that setting.