管程正确性的证明

作     者：John H.Howard 陈华瑛 

出 版 物：《计算机研究与发展》 (Journal of Computer Research and Development)

年 卷 期：1979年第5期

页      面：61-67页

主　　题：管程 定义 证明规则 历史变量 进程 队列长度 不变式 

摘      要：1.引言管程是为在多道程序系统中定义共享的抽象对象以及对它们的存取进行调度而设计的一种结构。*** 最近写的文章提供了管程的精确定义,并给出了几个管程用法的例子。Hoare 认为数据抽象和不变式这两种方法对大多数例子看来都是处理不了的。本文是对 Hoare 挑战的回答。本文描述了管程的一些重要性质的表示方法,并用Hoare 的公理系统来证明这些性质,还把这些方法应用于 Hoare 文章中举的几个例子,表明这些方法的实用性。本文提出的两种方法是:利用“历史变量来描述一个管程及使用它的进程过去所执行的操作序列;以及对管程的 Wait 和 Signal 操作的性质公理化,以便能用关于管程的形式断言来表达其调度性质。