The Beginnings of a Model for Atomicity Refinement of Expressions
 Lookup NU author(s)
 Dr Joey Coleman




Author(s)   Coleman JW 
Publication type   Report 
Series Title   School of Computing Science Technical Report Series 
Year   2009 
Legacy Date   March 2009 
Report Number   1147 
Pages   15 



Full text is available for this publication: 




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 Clike 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. 



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/1147.pdf 
Actions   