由莱斯利Lamport
ACM的来文，1989年2月，第32卷第1号，第32-45页
10.1145/63238.63240
评论
在过去的几年中，我开发了一种方法来实现并发系统的正式规范，我现在称之为
过渡公理方法。基本的形式主义已经在[12]和[1]中描述过了，但是形式的细节往往掩盖了重要的概念。在这里，我试图解释这些概念，而不讨论潜在形式主义的细节。
并发系统不容易指定。即使是一个简单的系统也可能是微妙的，并且通常很难找到使其易于理解的适当的抽象。指定一个复杂的系统是一项艰巨的工程任务。只有当复杂的结构是由简单的部分组成时，我们才能理解它们，所以指定复杂系统的方法必须有简单的概念基础。我将试图证明转移公理方法提供了这样一个基础。但是，我将不讨论与指定实际系统相关的工程问题。相反，这些概念将通过一系列的玩具示例来说明，这些示例并不意味着将被认真地视为真正的规格。
您是在提议一种规范语言吗?不。转换公理方法为编写形式化规范提供了概念和逻辑基础;它不是一种规范语言。方法决定了
什么说明书必须说明;语言决定细节
如何这是说。
您所说的正式规范是什么意思?我发现将规范视为系统用户与其实现者之间的契约是很有帮助的。契约应该告诉用户使用系统必须知道的一切，并且应该告诉实现者实现系统必须知道的一切。原则上，一旦这个契约达成一致，用户和实现者就不需要进一步通信了。(此视图描述
函数规范的;它并不意味着系统应该如何构建的范例。)
对于形式化的规范，实现是否满足规范的问题必须简化为断言在某些数学系统中是否可证明的问题。为了证明自己满足了合同的条件，实施者应该求助于逻辑而不是合同法。这并不意味着实现必须伴随着数学证明。这确实意味着，应该在原则上(尽管在实践中不一定)为正确的实现提供这样的证明。规范方法的形式化基础的存在是我所知道的保证规范是明确的唯一方法。
最终，我们指定的系统是物理对象，数学无法证明物理属性。我们只能证明系统的一个数学模型的性质;系统是否正确地实现了模型必须是一个法律问题而不是数学问题。
什么是系统?我所说的“系统”指的是任何在边界上以离散(数字)方式与其环境相互作用的东西。航空公司预订系统就是这样一个系统，使用该系统的代理(环境的一部分)和终端(系统的一部分)之间的界限可能被划定。Pascal过程是一个系统，它的环境是程序的其余部分，它通过响应过程调用和访问全局变量与程序交互。因此，指定的系统可能只是更大系统的一个组件。
一个真实的系统有很多属性，从它的响应时间到机柜的颜色。没有正式的方法可以指定所有这些属性。哪些可以用转移公理方法指定?转场公理方法指定了系统的行为，即系统与环境交互时执行的可观察操作序列。更准确地说，它指定了两类行为特性:安全性和活性特性。安全属性断言系统可以做什么，或者等价地说，系统不能做什么。部分正确是安全属性的一个例子，它断言程序可能不会产生错误的答案。活性属性断言系统必须做什么。终止是活属性的一个例子，它断言程序最终必须生成一个答案。(Alpern和Schneider[2]已经正式定义了这两类性质。) In the transition axiom method, safety and liveness properties are specified separately.
有一些重要的行为属性是不能用转移公理方法指定的;这包括平均响应时间和失败概率。转换公理规范可以提供一个正式的模型，用它来分析这些属性，
1但是它不能正式地指定它们。
还有一些重要的系统非行为属性可能需要指定，例如存储要求和机柜的颜色。这些完全不在本方法的范围之内。
为什么要分别指定安全性和活性特性?在过渡公理规范的基础上有一个单一的形式主义，因此在安全和活性属性规范之间没有正式的分离。然而，经验表明，对这两种性质的推断采用不同的方法，在实践中分离它们是方便的。我认为将规范分解为活性和安全特性的能力是该方法的优点之一。(为了验证活性性质，必须证明安全性质，但这是一个将证明分解为更小引理的过程。)
该方法可以指定实时行为吗?可以指定最坏情况行为，因为系统必须在一定时间内响应的要求可以表示为安全属性——即，在系统没有响应的情况下，时钟不允许达到某个值。平均响应时间不能表示为安全或活性属性。
转场公理方法可以断言某些动作要么必须发生(活动)，要么不能发生(安全)。它还能断言动作是可能发生的吗?不。规范作为系统行为的契约约束。断言系统可以或不可以做某事没有提供约束，因此没有作为正式规范的一部分发挥作用。包含此类断言的规范方法通常将它们用作活性属性的较差替代品。有些方法不能指定某个输入
必须产生一个特定的响应，而指定在输入之后可能会有响应。我遇到的每个使用这种断言的规范都通过用活性属性替换可能性断言而得到了改进，活性属性更准确地表达了系统的非正式需求。
不精确的措辞可能会使规范看起来包含可能性断言，而实际上并不包含。例如，有时有人指出传输线必须有可能丢失消息。然而，规范并不要求消息的丢失是可能的，因为这将禁止保证没有消息丢失的实现。规范可能要求在消息丢失的情况下发生某些事情(活动属性)或不发生某些事情(安全属性)。或者，消息可能丢失的声明可能只是关于规范的注释，注意到它不需要交付所有消息，并且不是实际规范的一部分。
如果一个安全属性断言某些行为不能发生，它的否定不就断言该行为是可能的吗?在一个正式的系统中，我们必须区分逻辑公式
一个来自断言⊢
一个，这意味着
一个是在逻辑上被证明的;⊢
一个不是逻辑本身的公式。在转移公理方法的逻辑基础上，如果
一个表示安全属性断言某些行动是不可能的，则否定
一个，这就是公式
一个，断言动作必须发生。该行动的可能性通过⊢的否定来表达
一个，这是一个元公式，而不是逻辑中的公式。有关更多详细信息，请参见[10]。
本文的全文是优质内容
没有发现记录
登录阅读全文
需要访问吗?
请选择以下选项之一，以访问优质内容和功能。
创建Web帐户
如果您已经是ACM会员，通信数码图书馆的订阅者，请建立一个网页帐户，以访问本网站的优质内容。
参加ACM
成为ACM的会员可以充分利用ACM杰出的计算信息资源、联网机会和其他好处。
订阅ACM通讯杂志
获得《中华文化纵横》50年以上的完整内容，每月获得印刷版。
购买这篇文章
非会员可以购买这篇文章或它所在的杂志。
