Comparing Degrees of Non-Determinism in Expression Evaluation

Comparing Degrees of Non-Determinism in Expression Evaluation
复制标题

比较表达式评估中的非决定论程度

DOI:
10.1093/comjnl/bxt005
复制
发表时间:
2013
期刊:
The Computer Journal
影响因子:
--
通讯作者:
Hayes I
Hayes I
中科院分区:
--
文献类型:
--
作者:
Hayes I

文献摘要

参考文献

被引文献

相似文献

编程语言中的表达式求值通常被认为是确定性的;然而,如果表达式涉及在其求值期间被进程环境修改的变量,则求值的结果可能是不确定的。发生这种情况的两种常见场景是并发程序,其中进程共享变量,以及交互以监视和/或控制其环境的实时程序。在这些上下文中,尽管表达式的任何特定求值都会给出单个结果,但根据环境对变量的修改与表达式求值中对变量的访问之间的相对时间,可能会返回一系列可能的值。要比较非确定性表达式计算的语义,可以使用表达式计算可能返回的可能值集。本文形式化的三种方法,非确定性表达式的评估,突出他们的共性和差异,显示的方法之间的关系,并探讨条件下,他们一致。模态算子表示谓词对所有可能的评价和对某些可能的评价都成立,并与每种评价方法相关联,研究了这些算子之间的性质和关系。此外,链接到一个新的符号用于推理干扰。
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 non-deterministic. 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 of a variable by the environment and its access within the expression evaluation. To compare the semantics of non-deterministic expression evaluation, one can use the set of possible values the expression evaluation could return. This paper formalizes three approaches to non-deterministic 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.
DOI: --
发表时间: 2001
期刊: Acta Informatica
影响因子: 0.6
作者:
I. Hayes;M. Utting
通讯作者: M. Utting
依赖/保证上下文中的表达式分解
DOI: --
发表时间: 2008
期刊: Verified Software: Theories, Tools, Experiments
影响因子: --
作者:
Joey W. Coleman
通讯作者: Joey W. Coleman
对偶非确定性函数
DOI: --
发表时间: 2008
期刊: TOPL
影响因子: --
作者:
Joseph M. Morris;M. Tyrrell
通讯作者: M. Tyrrell
DOI: --
发表时间: 1964
期刊:
影响因子: --
作者:
J. McCarthy
通讯作者: J. McCarthy
根据控制系统的环境规格确定控制系统的规格
DOI: --
发表时间: 2003
期刊: FME
影响因子: --
作者:
I. Hayes;M. Jackson;Cliff B. Jones
通讯作者: Cliff B. Jones