The Beginnings of a Model for Atomicity Refinement of Expressions

  1. Lookup NU author(s)
  2. Dr Joey Coleman
Author(s)Coleman JW
Publication type Report
Series TitleSchool of Computing Science Technical Report Series
Year2009
DateMarch 2009
Report Number1147
Pages15
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 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.
InstitutionSchool of Computing Science, University of Newcastle upon Tyne
Place PublishedNewcastle upon Tyne
URLhttp://www.cs.ncl.ac.uk/publications/trs/papers/1147.pdf
ActionsLink to this publication