Toggle Main Menu Toggle Search

ePrints

Guaranteeing the soundness of rely/guarantee rules

Lookup NU author(s): Dr Joey Coleman, Professor Cliff Jones

Downloads


Abstract

The challenges of finding compositional ways of (formally) developing concurrent programs are considerable. One way of tackling such design tasks is to deploy rely and guarantee conditions to record and reason about interference. This paper presents a new approach to justifying the soundness of rely/guarantee inference rules. The approach followed is to view a “structural operational semantics” as defining an inference system and to show that the proof rules used are valid proof tactics within that inference system. This leaves aside worries about completeness of the rely/guarantee rule set because one is always in a position to add new rules in the same way.


Publication metadata

Author(s): Coleman JW, Jones CB

Publication type: Report

Publication status: Published

Series Title: School of Computing Science Technical Report Series

Year: 2006

Pages: 23

Print publication date: 01/03/2006

Source Publication Date: March 2006

Report Number: 955

Institution: School of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne

URL: http://www.cs.ncl.ac.uk/publications/trs/papers/955.pdf


Share