Abstraction and verification in Alphard: Defining and specifying iteration and generators
Abstraction and verification in Alphard: Defining and specifying iteration and generators
复制标题
Alphard 中的抽象和验证：定义和指定迭代和生成器
DOI：
10.1145/800022.808321
复制
发表时间：
1977
期刊：
影响因子：
--
通讯作者：
R. L. London
中科院分区：
文献类型：
--
作者：
M. Shaw;Wm. A. Wulf;R. L. London
Alphard表单为程序员提供了对抽象数据类型实现的大量控制。在本文中，我们扩展的抽象技术，从简单的数据表示和函数定义的迭代语句，数据和语言本身的控制结构之间的相互作用的最重要的点。我们介绍了一种专门的Alphard循环操作抽象实体，而不明确依赖于这些实体的表示。我们开发的规范和验证技术，允许这样的迭代发电机的属性表示的形式证明规则。我们得到的结果，这些循环的共同特殊情况下，基本上是相同的，在其他语言中的相应结构。我们还提供了一种显示生成器将终止的方法。
The Alphard form provides the programmer with a great deal of control over the implementation of abstract data types. In this paper we extend the abstraction techniques from simple data representation and function definition to the iteration statement, the most important point of interaction between data and the control structure of the language itself. We introduce a means of specializing Alphard's loops to operate on abstract entities without explicit dependence on the representation of those entities. We develop specification and verification techniques that allow the properties of the generators for such iterations to be expressed in the form of proof rules. We obtain results for common special cases of these loops that are essentially identical to the corresponding constructs in other languages. We also provide a means of showing that a generator will terminate.