Email Gateway (Oct 20 2021 at 10:02): Email Gateway (Oct 20 2021 at 10:02):From: Tobias Nipkow <nipkow@in.tum.de>
Algebras for Iteration, Infinite Execut ions and Correctness of Sequential
Computations
Walter Guttmann
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.
https://www.isa-afp.org/entries/Correctness_Algebras.html
Enjoy!
smime.p7s
Last updated: Jan 04 2025 at 20:18 UTC