Email Gateway (Aug 22 2022 at 14:56): Email Gateway (Aug 22 2022 at 14:56):From: Tobias Nipkow <nipkow@in.tum.de>
Concurrent Refinement Algebra and Rely Quotients
Julian Fell, Ian Hayes, Andrius Velykis
The concurrent refinement algebra developed here is designed to
provide a foundation for rely/guarantee reasoning about concurrent
programs. The algebra builds on a complete lattice of commands by
providing sequential composition, parallel composition and a novel
weak conjunction operator. The weak conjunction operator coincides
with the lattice supremum providing its arguments are non-aborting,
but aborts if either of its arguments do. Weak conjunction provides an
abstract version of a guarantee condition as a guarantee process. We
distinguish between models that distribute sequential composition over
non-deterministic choice from the left (referred to as being
conjunctive in the refinement calculus literature) and those that
don't. Least and greatest fixed points of monotone functions are
provided to allow recursion and iteration operators to be added to the
language. Additional iteration laws are available for conjunctive
models. The rely quotient of processes c and
i is the process that, if executed in parallel with
i implements c. It represents an
abstract version of a rely condition generalised to a process.
https://www.isa-afp.org/entries/Concurrent_Ref_Alg.shtml
Enjoy!
smime.p7s
Last updated: May 01 2024 at 20:18 UTC