ePrints

Designing an unbounded buffer in rely-guarantee

Lookup NU author(s): Diego Machado Dias, Dr Leo Freitas

Downloads

• Published version [.pdf]

Abstract

We use a variety of consumer-producer specifications to illustrate the range of choices and rationale that arise in concurrent specifications using rely-guarantee. We also extend postconditions with a new argument to make explicit the environment assigned to the process, and present a semantics for possible values that explores the new parameter in postconditions. All specifications presented in this document were mechanised in Isabelle/HOL.

Publication metadata

Author(s): Dias D, Freitas L

Publication type: Report

Publication status: Published

Series Title: School of Computing Science Technical Report Series

Year: 2014

Pages: 39

Print publication date: 01/09/2014

Report Number: 1431

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/1431.pdf

Share