| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Concurrent Refinement Algebra and Rely Quotients
| Title: | Concurrent Refinement Algebra and Rely Quotients |
| Authors: | Julian Fell (julian /dot/ fell /at/ uq /dot/ net /dot/ au), Ian J. Hayes (ian /dot/ hayes /at/ itee /dot/ uq /dot/ edu /dot/ au) and Andrius Velykis |
| Submission date: | 2016-12-30 |
| Abstract: | 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. |
| BibTeX: |
@article{Concurrent_Ref_Alg-AFP,
author = {Julian Fell and Ian J. Hayes and Andrius Velykis},
title = {Concurrent Refinement Algebra and Rely Quotients},
journal = {Archive of Formal Proofs},
month = dec,
year = 2016,
note = {\url{http://isa-afp.org/entries/Concurrent_Ref_Alg.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |