Browse by author
Lookup NU author(s): Professor Ian Hayes, Emeritus Professor Cliff JonesORCiD
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
Expression evaluation in programming languages is normally assumed to be deterministic; however, if an expression involves variables that are being modified by the environment of the process during its evaluation, the result of the evaluation can be nondeterministic. Two common scenarios in which this occurs are concurrent programs within which processes share variables and real- time programs that interact to monitor and/or control their environment. In these contexts, although any particular evaluation of an expression gives a single result, there is a range of possible values that could be returned depending on the relative timing between modification to a variable by the environment and its access within the expression evaluation. To compare the semantics of nondeterministic expression evaluation, one can use the set of possible values the expression evaluation could return. This paper formalises three approaches to nondeterministic expression evaluation, highlights their commonalities and differences, shows the relationships between the approaches and explores conditions under which they coincide. Modal operators representing that a predicate holds for all possible evaluations and for some possible evaluation are associated with each of the evaluation approaches, and the properties and relationships between these operators are investigated. Furthermore, a link is made to a new notation used in reasoning about interference.
Author(s): Hayes IJ, Burns A, Dongol B, Jones CB
Publication type: Article
Publication status: Published
Journal: The Computer Journal
Year: 2013
Volume: 56
Issue: 6
Pages: 741-755
Print publication date: 05/02/2013
ISSN (print): 0010-4620
ISSN (electronic): 1460-2067
Publisher: Oxford University Press
URL: http://dx.doi.org/10.1093/comjnl/bxt005
DOI: 10.1093/comjnl/bxt005
Altmetrics provided by Altmetric
