Unifying Theories of Programming That Distinguish Nontermination and Abort
Unifying Theories of Programming That Distinguish Nontermination and Abort
复制标题
区分非终止和中止的统一编程理论
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
L. Meinicke
中科院分区：
文献类型：
--
作者：
I. Hayes;S. Dunne;L. Meinicke
在本文中，我们关注一些规范模型之间的关系。这些模型是依据霍尔（Hoare）和何（He）的统一程序设计理论构建的，但与广泛使用的规范模型相对应。我们涵盖了诸如部分正确性、完全正确性和一般正确性等问题。
我们用于区分这些模型的特性如下：
- 它们是否允许对初始状态进行假设规范，在该初始状态之外不保证程序的行为，即程序可能“中止”；
- 一个规范是否可能允许甚至要求不终止作为一种有效的（非中止的）结果；
- 它们是否允许表达测试或使能条件，在这些条件之外程序没有可能的行为。
在考虑终止时，我们既考虑一个抽象模型，该模型仅区分程序是否终止，也考虑包含时间概念的模型：要么是代表进展概念的抽象时间，要么是实时。
In this paper we focus on the relationship between a number of specification models. The models are formulated in the Unifying Theories of Programming of Hoare and He, but correspond to widely used specification models. We cover issues such as partial correctness, total correctness, and general correctness.
The properties we use to distinguish the models are these: - whether they allow the specification of assumptions about the initial state outside of which no guarantees are given about the behaviour of the program, i.e., the program may "abort"; - whether a specification may allow or even require nontermination as a valid (non-aborting) outcome; and - whether they allow the expression of tests or enabling conditions, outside of which the program has no possible behaviour.
When considering termination, we consider both an abstract model, which only distinguishes whether a program terminates or not, as well as models that include a notion of time: either abstract time representing a notion of progress or real-time.
DOI：
10.1007/978-3-642-14521-6_4
发表时间：
2010
期刊：
--
影响因子：
--
作者：
Cavalcanti A
通讯作者：
Cavalcanti A
DOI：
10.1007/978-3-642-13321-3_5
发表时间：
2010
期刊：
--
影响因子：
--
作者：
Boiten E
通讯作者：
Boiten E