Toggle Main Menu Toggle Search

Open Access padlockePrints

The Beginnings of a Model for Atomicity Refinement of Expressions

Lookup NU author(s): Dr Joey Coleman



This technical report is a record of progress made by the author on addressing the semantic gap between the atomicity assumptions made in formal methods and those (i.e. the lack of, entirely) made in the design and implementation of common programming languages. A semantics for expression evaluation which models the characteristics of C-like languages - including accounting for the effect of interference during evaluation - is given as an initial model. This is used to introduce the notion of interference paths: by explicitly mapping out the effects of interference a sequence of states can be generated. These sequences can then be used to build a refinement relation between expressions; this refinement relation can be used to develop initial specifications with strong atomicity assumptions and then refine them into specifications with weaker assumptions. However, the model of interference paths requires a strong constraint on the form of expression used so a discussion of the steps necessary to relax the constraint is given; however, this last is ongoing work and still contains unresolved issues.

Publication metadata

Author(s): Coleman JW

Publication type: Report

Publication status: Published

Series Title: School of Computing Science Technical Report Series

Year: 2009

Pages: 15

Print publication date: 01/03/2009

Source Publication Date: March 2009

Report Number: 1147

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

Place Published: Newcastle upon Tyne