On Rely-Guarantee Reasoning
| Autor: | Stephan van Staden |
|---|---|
| Rok vydání: | 2015 |
| Předmět: |
Soundness
Theoretical computer science business.industry Semantics (computer science) Computer science Binary relation Concurrency Judgement HOL 020207 software engineering 0102 computer and information sciences 02 engineering and technology 16. Peace & justice Mathematical proof 01 natural sciences Operational semantics 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0202 electrical engineering electronic engineering information engineering Artificial intelligence business |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783319197968 MPC |
| DOI: | 10.1007/978-3-319-19797-5_2 |
| Popis: | Many semantic models of rely-guarantee have been proposed in the literature. This paper proposes a new classification of the approaches into two groups based on their treatment of guarantee conditions. To allow a meaningful comparison, it constructs an abstract model for each group in a unified setting. The first model uses a weaker judgement and supports more general rules for atomic commands and disjunction. However, the stronger judgement of the second model permits the elegant separation of the rely from the guarantee due to Hayes et al. and allows refinement-style reasoning. The generalisation to models that use binary relations for postconditions is also investigated. An operational semantics is derived and both models are shown to be sound with respect to execution. All proofs have been checked with Isabelle/HOL and are available online. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|