抽象命令语言：正确性检查和实现

104理论计算机科学电子笔记42（2001）网址：http://www.elsevier.nl/locate/entcs/volume42.html20页抽象命令：规范和实现史蒂夫·邓恩1计算与数学学院，提赛德米德尔斯堡大学，TS1 3BA，英国摘要总的正确性和一般的正确性进行检查，后者被提升为更合适的语义基础的程序，包括基本的顺序交互组件的今天的典型的高度分布式系统，在某些时候，非终止实际上可能需要。 为此，我们提出了一种新的抽象程序设计语言，我们的抽象命令语言，定义了一个完整的一般正确性语义，和一个适当的概念的细化，保持一般的正确性，在这方面，我们的语言的所有构造函数是单调的。这为抽象规范提供了统一的符号，抽象规范表达了这种非终止性要求及其逐步和分段细化为满足这种要求的可执行实现。此外，我们ill-lustrate使用我们的语言的构造函数，音乐会，这使得这种非终止性的要求出现在分段细化，我们通过一个原始的并发形式来描述其实现。1介绍1996年，在研究B方法中的精化时，我们遇到了一类程序，最终被称为半判定2程序，其抽象规范既不能用B的抽象机器符号表示，也不能调查很快确定，不可表达性不仅仅是B的特定符号中的一个具体缺点1电子邮件：s.e. tees.ac.uk一个可判定的程序总是以一个正确的结果结束。一个半可判定的程序要么以正确的结果结束，要么根本它永远不会终止，即使是流产，也不会得到不正确的结果。2001年由ElsevierScien ceB出版。 诉 操作访问和C CB Y-NC-N D链接。杜内105成立。因此，这是B与许多其他形式开发方法共享的限制，这些方法像B一样，建立在完全正确性的基础上。我们首先把注意力集中在如何在B的上下文中具体地弥补这个缺点上，我们的初步建议发表在[7]中。我们的思想在[8]中得到了进一步的改进，以提供B的广义替换的一般正确性对应物，我们称之为本文通过将ab-decision命令置于独立于B的正式基础上来巩固这项工作，为表达和推理这种半可判定性提供统一任何抽象层次的程序在下文中，我们首先对谓词- Transformer语义进行简要的历史评价，这导致了当前完全正确性和一般正确性学派之间的二分法我们认为，正是一般的正确性使我们获得了行为描述的精细颗粒，这是顺序程序开发人员所需要的，这些程序包括当今日益分布式和相互通信的系统的基本交互构建块论文的后半部分详细介绍了抽象命令的语法和语义，特别是定义和讨论了语言的每个结构。2部分和完全正确性Dijkstra [3]在1976年为程序引入的著名的最弱前提（wp）谓词转换器语义，随后由Gries在[10]中广泛传播，是完全正确性的语义。它告诉我们在什么样的起始条件下，程序将保证给出满足给定后置条件的结果。一个要求不太高的语义称为部分正确性，其特征在于第二个谓词转换器，Dijkstra也描述过，但 他称之为最弱自由前提（wlp）谓词转换器。它告诉我们，在什么样的开始条件下，一个程序可以被依赖于提供一个满足给定后置条件的结果，只要它终止- 也 就 是 说 ， 当 它 可 以 被 依 赖 于 至 少 不 提 供 一 个 与 给 定后 置 条 件 相 矛 盾 的 结 果 。完全正确和部分正确显然是密切相关的。它们之间的区别是程序是否会终止并因此产生任何结果的问题但是，仅仅通过搁置终止问题，不能简单地从完全正确中提取也不能完全从部分正确性重建完全正确性我们将写wp（A，Q）来表示程序A建立后置条件Q的最弱前置条件，因此，特别地，wp（A，true）表示A建立true的最弱前置条件，即确定以任何结果终止。相应地，我们将写wlp（A，Q）来表示A“自由地”建立的最弱前提条件杜内106∧Q，也就是说，如果Q终止，则建立Q。虽然谓词变换词wlp（A，）和wp（A，）都是正合取的，也就是说它们分布在非空合取词上，但只有wlp（A，）是泛合取的，也就是说它还将空合取词true映射到自身。这两个谓词-转换词之间的必然逻辑关系用规律wp（A，Q） =wp（A，true）wlp（A，Q）.程序A的终止谓词wp（A，true）有时写为trm（A）。上述定律暗示了wlp比wp更基本。我们可以将trm（A）和wlp（A，）作为A的基本特征，然后简单地将wp（A，Q）定义为trm（A）wlp（A，Q）。事实上，这就是我们在本文后面定义抽象命令时选择采用的方法3一般正确性到1990年[4]出现的时候，也就是[3] 14年之后，Dijk-stra显然已经得出了这样的观点，即完全描述顺序程序行为的语义必须包含完全正确性和部分正确性。因此[4]给出了保护命令语言中每个构造的wp和wlp解释。类似地，Nelson [22]在他对Dijkstra的calculus的开创性概括中使用了wp和wlp来承认具有奇迹般行为和无界非决定性的抽象程序。如今，由Jacobs和Gries [18]创造的术语一般正确性表示结合了部分正确性和完全正确性的语义。然而，并不是每个人都遵循Dijkstra和Scholten以及Nelson的领导，采用一般正确性作为顺序程序的基准语义最著名的形式定义学派，包括B[1]、VDM [19]、Z [23]和精化演算[21]，都坚持纯粹基于完全正确性的令人惊讶的是，即使是Hoare和He [17，16]最近关于统一编程理论的工作也忽略了一般正确性。事实上，在[17]中，他们公布了一个健康条件，H2，明确禁止将非终止性作为一个实际要求，从而确保只有完全正确的设计在下一节中，我们将讨论为什么这种对完全正确性的排他性坚持可能不适合今天的许多旁白：关于霍尔和He统一理论本身如何在不损害其有效性或优雅性的情况下加以调和，以承认广义正确性设计的更广泛的谓词类别的有趣问题，我们已经在[5]中讨论过了。我们在这里不追求它。杜内1074互动时代米尔纳曾说过，今天的计算就是交互。3这对软件开发人员有重要的意义。例如，我们不再总是必须只关心执行我们的顺序程序直到成功终止的结果。这样的程序提供了当今复杂的分布式处理系统的独立的交互线程，因此我们可能要求它们即使在终止甚至没有前景的情况下也能可靠地工作。例如，通道侦听器必须空闲，直到它检测到传入消息，然后在消息到达时但是，由于从来没有人能保证这样的信息会到达，我们的通道监听器原则上必须能够无限地空转。因此，在某些情况下，不终止正是我们所要求的。作为正式的软件规范者和设计者，我们必须有一种规范语言，我们可以用它来正式地表达这样的需求，还有一种设计演算，我们可以用它来证明给定的程序满足这样的规范。引用Hehner和Gravell的话[15]：由于通信的增加，非终止执行可以执行有用的计算，因此不坚持终止的语义是有用的。我们会更进一步说，我们需要一个语义学，在这个语义学中，我们可以在某些条件下坚持非终止性简而言之，我们必须学会在普遍正确的背景下工作在这一点上，还应指出各种作者在时间细化领域所做的工作，例如Hayes [11，12]和Hehner [13，14]。这样的工作总是表现出关键的一般正确性charteristic真正的非终止是准确的特点。另一方面，完全正确只能将非终止性转化为完全不可预测的行为，即所谓的发散或混沌。一般正确性可以被隐含地说成拥有一个非常粗粒度的时间域，只有三个值：零（计算时间细化可以被视为建立在一般正确性模型的一个精心设计的变体之上，在这个变体中，时间被赋予了一个更细粒度的连续值。5细化在[21]中，摩根主张抛弃程序和规范之间：他说，所有程序都是程序，尽管分布在广泛的细化范围内;有些程序更抽象，而3河米尔纳，美国空军科学院21周年研讨会讲话，英国皇家学会，伦敦，21998年12杜内108±其他的更具体，后者中的一些是直接可执行的。同样，在[2]中，Back和Butler说，在精化演算中，程序所需的行为被指定为一个抽象的、可能不可执行的程序，然后通过一系列保持正确性的变换将其精化为一个高效的、可执行的程序。正确性保持变换的概念由程序之间的精化关系来建模，该关系是传递的，因此支持逐步精化，并且相对于程序构造器4是单调的，因此支持分段精化。从现在起，我们将在这种抽象的意义上使用程序这个术语摩根通过他发明的规范语句来扩充Dijkstra很自然地，由于当时他所知道的保护命令的语义是完全正确的，摩根只赋予他的具体化语句一个完全正确的语义。大约在同一时间，Abrial发明了一般化的替换，作为软件开发B方法中抽象机器符号的基础[1]。这些可以用来描述与指定语句相同范围的抽象程序，但在更统一的符号中，可以在很大程度上与具体程序共享这种一致性是Abrial就像摩根的具体化陈述一样，阿布里亚尔只给了他的广义替换一个完全正确的语义。正如我们在引言中已经指出的，我们的抽象命令最初是作为Abrial的广义替换的直接广义正确性对应物而受到启发的一般正确性精化是完全正确性精化的自然扩展。如果A和B是同一程序空间上的一般正确的规范，那么A被B定义，写为AB，如果B的每一个可能的行为也是A的可能行为。形式上，这是通过断言对于程序空间上的每个后置条件Qwp（A，Q）<$wp（B，Q）和wlp（A，Q）<$wlp（B，Q）。一般正确性程序在这种精化关系下形成一个完整的格Dijkstra和Scholten另一方面，Nelson对保护命令语言的推广[22]确实给了它两个新的成分：一个包含抽象程序的它[4]当然，它们的意思是，程序构造器相对于加细关系是单调的杜内109不幸的是，Nelson最重要的是如果...菲兰德·杜... od，因为从A±B中，我们既不能推断出如果A f ± 如果B fnordo A od±doB od。因此，Nelson6一般正确性迭代当我们从完全正确性转向一般正确性时，程序的精化排序不再适合作为标准最小不动点处理迭代的基础，作为递归的特殊情况例如，它将无限循环程序while true doskip end我们的抽象命令语言与完全混乱的程序，我们称之为无政府状态，这是我们的细化底部。但是，至少从操作上讲，我们的无限循环是完全确定的，因为它永远不会终止。一般正确性必须忠实地遵守其保证的不终止性。正如Nelson在[22]中解释的那样，实现这一点的标准方法是使用- other排序并将递归定义为关于此的最小固定点这里讨论的排序是所谓的Egli-Milner近似排序：当A和B是程序时，我们说A近似B，如果对于每个后置条件Qwp（A，Q）<$wp（B，Q）和wlp（B，Q）<$wlp（A，Q）。虽然乍一看，这与我们先前的细化排序非常相似，但请注意这两个含义现在处于相反方向的关键区别我们的无限循环是Egli-Milner排序的底部，因为它近似于每一个程序，而细化底部无政府状态仅近似于一小类程序，无论何时终止，它们的结果都没有任何约束事实上，稍后我们将使用自然归纳法建设性地定义抽象命令迭代他的命令语言。因此，我们避免求助于Egli-Milner排序和不动点理论。然而，要在我们的抽象命令语言中引入更完整的递归概念，我们必须使用Egli-Milner。杜内110⊆\∪|7抽象命令主动框架的概念首先由我们在[6]中引入，用于一般化的替换。我们现在也将其用于抽象命令。我们将变量的集合称为框架。如果框架仅包括一个变量，则框架及其单个组成变量是同义的。如果u和v是帧，则u v表示通过合并u和v而获得的新帧，并且u v表示通过从u中移除其与v共享的任何变量而获得的残余帧。我们说标架v延伸标架u如果u v。我们用表示空框架。抽象命令总是在由一组变量提供的上下文中解释，这些变量构成了范围内所有变量的全局参考框架或字母表。如果我们必须明确地把它作为一个框架，我们用α来表示字母表。我们假设，没有明确地定义它，一个隐含的全序的字母表，使我们能够使用框架作为向量变量在一个明确的方式。我们把一个ab命令作用于其上的变量字母表中的集合称为它的框架。我们的操作直觉是，这些是命令可以赋值的变量我们用frame（A）表示抽象命令A的一个抽象的命令可以被动地引用其框架之外的字母表中的变量例如，x：=y的框架就是x，尽管它也被动地引用了y。帧可以是空的，如skip中，或者如x7skip中，其仅被动引用x。<我们区分skip和x：=x，因为它们有不同的框架。现在我们可以继续定义构成抽象命令语言的基本命令和构造函数为了便于参考，我们将它们全部列在表1 抽象命令A的含义包括三个不同的元素：它的框架frame（A），它的终止trm（A）和它的最弱自由前提谓词变换器wlp（A），它作用于后置条件，即当前字母表上的谓词。伴随以下定义的，往往是对有关命令的作战解释。这样的解释只是为了帮助我们对命令的直觉它们从来不是命令定义的必要部分，命令定义总是根据上述三个skip：正如人们可以从它的名字skip中推断出的那样，skip什么也不做，因此很容易混淆：frame（skip）是空帧，trm（skip）总是为真，wlp（skip，）是身份谓词Transformer。所以我们有frame（skip） = 0，trm（skip） =true，wlp（skip，Q）=Q。杜内111⟨⟩|名称语法skipskip分配x：=E预处理命令保护命令有界选择P|一P=AA[]B条件如果P那么A否则B结束短条件如果P那么A结束无限选择@z。一顺序组合有限重复A;BAn不定赋值重复闭合x：PA.迭代当P做A结束时平行作曲音乐会一||BA#B表1抽象命令语言赋值：采用x：=E的形式，其中E是一个定义良好的适当类型的表达式。x：=E的框架是x，它总是终止。 谓词转换器wlp（x：=E，）是根据句法替换Q E/x来定义的，它表示Q，其中x的每个自由出现都被E替换。所以我们有frame（x：=E）=x，trm（x：=E）= true，wlp（x：= E，Q） =QE/x.预处理命令：采用形式P A，其中P是谓词，A是抽象命令。前提条件P仅仅具有加强A杜内112⇒⇒|⇒−→|⇒因此我们框架（P|A）=帧（A），trm（P|A）= Ptrm（A），wlp（ P |A ， Q ） = wlp （ A ，Q）。保护命令：采用P=A的形式，其中P是谓词，A这是一个抽象的命令。后卫P限制了A我们有frame（P=A）=frame（A），trm（P = λA） =Pλtrm（A），wlp（P = λA，Q）=P λ wlp（A，Q）.特别是，形式P=skip是我们的抽象命令语言中历史上被称为Floyd假设的表现形式[9]。在我们的一般正确性语义中，前提条件和守卫之间的相互作用给了我们重要的表达能力。通过预处理一个受保护的命令，我们可以表示有保证的非终止性。例如，我们定义一个程序从来不never=false |false =跳过。我们可以很容易地从这个定义中证明，trm（never）= false，对于任何Q，wlp（never，Q）= true，这意味着never永远不会被保证终止，但是如果它终止了，它会给我们任何我们要求的结果（即使我们要求不可能的结果，满足false的结果）。我们得出结论，事实上，永远不会终止。它的定义是有趣的形式P P=的一个极端例子。 它规定了像A这样的行为， P持有并保证在P之外不终止。这对应于Dijkstra和Scholten [4]以及Nelson [22]在保护命令语言中赋予ifP A如果我们再次跳过A，精明的读者这次会认出PP=skip是Floyd断言[9]。有界选择：采用A[]B的形式，其中A和B是抽象命令。它代表了一个恶魔在A和B之间的选择。它们的帧是合并的，所以我们有frame（A[]B）=frame（A）≠frame（B），trm（A[]B）=trm（A）<$trm（B），wlp（A [] B，Q） =wlp（A，Q）<$wlp（B，Q）.杜内113条件：采用熟悉的形式ifG thenA elseB end，其中G是谓词，A和B是抽象命令。其定义为：if G then A else B end= （G =<$A）[]（<$G =<$B）.Abrial在[1]中在广义置换的上下文中给出了类似的定义正如Abrial所指出的，这样的定义很有趣，因为它揭示了长期以来被程序员视为基本编程结构的东西实际上只是两个更基本的结构的组合，即守护和非确定性选择。短条件句：采用熟悉的形式ifG thenA end，其中G是谓词，A是抽象命令。其定义为：如果G那么A end = （G =<$A）[]（<$G =<$skip）.unboundedchoice：采用@z的形式。其中A是一个抽象命令，z相对于当前字母表是新的。A的字母表被理解为当前字母表增加了z。无限的选择@z。 A代表A被恶魔选择变量z的任意值所衰减。@ z的框架。A是通过从A的标架中去掉z得到的，如果z在那里的话。因此我们frame（@z. A）=frame（A）\z，trm（@z. A）=λz·trm（A），wlp（@z. A，Q） =λz·wlp（A，Q）。这个结构得名于这样一个事实，即如果z的范围在一个无限值域内，那么选择将是无限不确定的。因此，它可能打破Dijkstra顺序组合：采用A;B的形式，其中A和B是抽象命令。它表示A的执行，然后是B。A和B的帧被合并，并且A;B在A终止的地方终止，并且保证建立B所以我们有frame（A;B）=frame（A）≠frame（B），trm（A;B）=trm（A）wlp（A，trm（B）），wlp（A; B，Q）=wlp（A，wlp（B，Q））。有限重复：采用An的形式，其中A是抽象命令，n是自然数。它表示A的n次连续执行。我们根据顺序组合归纳地定义An如下：A0=跳过，An+1= A; An.杜内114⇒⇒8健全性既然我们已经定义了一些具体的抽象命令，那么就应该提出这些定义的合理性问题一般来说，当定义一个新的抽象命令A时，我们是否必须尊重frame（A）、wlp（A，）和trm（A）上的任何约束，或者我们可以任意定义它们中的每一个？事实上，我们可以任意指定trm（A）作为alpha- bet上的任何谓词，但是，正如我们在第2节中已经注意到的，wlp（A，）必须是泛合取的。此外，在框架（A）和wlp（A，Q）之间存在一个相互约束，称为框架一致性，它确保A不能对其框架之外的变量施加不适当的影响：如果Q是独立于框架（A）的后置条件，因为框架（A）的变量在Q中没有自由，那么wlp（A，Q）必须是Q的衰减或弱化：换句话说，Q wlp（A，Q）必须保持。对于许多命令，衰减将是微不足道的，因为Q=wlp（A，Q）成立，但当A不可行时，会出现严格的削弱。例如，wlp（false =skip）将任何Q完全衰减为真。通过本文中定义的抽象命令语言构造函数可表达的任何抽象命令A都必须满足(i)wlp（A，）分布在任意合取上，并且(ii)对于任何与标架（A）无关的Q，Q ∈ wlp（A，Q）成立。9抽象命令细化我们现在提出一个重要的问题，即一个命令细化另一个命令意味着什么。在前面，我们介绍了广义正确性修正的概念，但我们只是在同一程序空间上定义了它。这给了我们一个合适的概念来细化共享同一框架的抽象命令，然而，如果我们的抽象命令语言要提供一个完整的程序开发环境，我们需要的不仅仅是这个。对字母表上所有抽象命令的细化的综合概念必须考虑框架。例如，我们可以用x：=x来精化skip，或者确实用skip来精化x：=x吗？事实上，抽象命令细化的额外成分涉及框架包含。因此，如果A和B是相同字母表上的抽象命令，则A被B精化，记为A±B，当且仅当，对于字母表上的每个后置条件Qtrm（A）trm（B），wlp（A，Q）=wlp（B，Q），以及框架（A）和框架（B）。在我们的抽象命令refinementskip下，实际上是由x：=x来进行 refinement的。但反过来就不是这样了。所有抽象命令语言构造函数杜内115/对于我们的抽象命令细化，本文中定义的是单调的。抽象命令refinemnt的框架扩展方面确保了我们将在第12节中定义的并行组合是单调的。10特征等同器械我们已经遇到了抽象命令A的一个基本谓词：它的终止谓词trm（A），它表征了A的执行从哪里保证终止，因此不会有不终止的风险其他几个重要的特征谓词与A有关.它们中的大多数的名称都像[1]中的trm一样被采用，在那里它们被用于为广义置换定义的相应谓词。fis（A）：可行性谓词fis（A）描述了A的执行是可行的（非奇迹）。记住，一个程序在它可以保证建立false的地方表现得很神奇，所以我们定义它为：fis（A）=<$wp（A，false），或者等价地，fis（A）=wlp（A，false）.cic（A）：永久谓词cic（A）描述了抽象命令A的永久重复是可行的。（cic这个名字是“循环和无限链”的首字母缩写其定义为：cic（A）= Nat·fis（An）。saf（A）：安全性谓词saf（A）表征了A的任何有限重复在哪里是安全的，不存在非终止性风险。我们将其定义为saf（A）= Nat·trm（An）.prd（A）：前后谓词prd（A）将A的帧中的变量的前值与它们在执行A之后的潜在后值相设frame（A）由x表示，则我们定义prd（A）为：p rd（A）=<$wlp（A，xi=XI）.其中XJ相对于当前字母表是新的，并且表示X的后值。谓词x=xJ称为前后差异y。对于包括变量x，y的帧，前后差异将是x，yj=xJ，yJ，其中h扩展到f（x=xJ，y=yJ）。在发生紧急情况时，杜内116⇒⇒在一个空框架中，合取词退化为真，因此与空框架相关联的前后差异为假。因此，例如，prd（skip）=<$wlp（skip，false）=<$false=true。如果框架（A）是已知的，那么prd（A）和wlp（A，）携带关于A的等价信息，使得每个都可以从另一个导出。例如，如果frame（A）是x，我们有wlp（A，Q） = x J·prd（A）<$Q <$x J/x <$.这是有用的，因为有时当我们希望引入一个新的抽象命令A时，指定prd（A）比指定wlp（A，）更方便。11恶魔与奇迹我们用来分解传统条件句的守卫命令和恶魔选择之间的相互作用，巧合的是，恶魔的选择在可行性方面是天使的当我们把无处不在的神奇抽象命令魔法（= false =skip）与任何抽象命令A一起用于恶魔选择时，这一点就得到了非常明显的说明。很容易证明，魔法=A。恶魔当被迫在奇迹和可行的选择之间做出选择时，他必须总是选择后者。事实上，恶魔受到的约束比他面临的直接选择所表现出来的要大得多：如果他在两个明显可行的直接选择中做出选择，那么其中一个选择可能会导致一个不可行的命令，也许是很晚的时候，在程序中即使是这种拖延的不可行性，例如，很容易证明该程序（x：= 1 []x：= 2）;x= 1 =跳过等于x：= 1。 Nelson [22]建议我们采用两种等价的关于恶魔行为的操作直觉中的任何一种。我们可以认为他有一种透视能力，可以看到程序未来的执行过程，预见到采取特定选择可能导致的任何不可行性，从而避免这种选择。或者，我们可以想象他盲目地做出选择，但如果随后遇到不可行性，执行将回溯，让他重新考虑在上面的小程序中，我们观察到x= 1 =skip充当了一个回顾性的杜内11712更多抽象命令不确定赋值：采用x：P的形式，其中x是当前字母表中的变量，P是当前字母表加上xJ上的谓词。它表示将满足P的任意xJ值赋值给x。我们有frame（x：P）= x，trm （ x ： P ） =true，prd（x：P）=P。不确定赋值不是基本的抽象命令。我们可以等价地定义它为x：P= @xJ. P =x：= xJ.我们可以用以下形式表示任何抽象命令A，其中frame（A）=xtrm（A）|x：prd（A），它为抽象命令提供了有用的范式它还提供了一种方便的方法来定义我们的细化底层命令无政府状态，anarchy =false |α：真。这是我们必须明确提到的极少数情况之一，α，我们的字母框架。repeating closure：采用A闭包的形式，其中A是一个抽象命令。它代表了A的任意重复：也就是说，对A的任何有限重复甚至永久重复的恶魔选择。我们有frame（A）=frame（A），trm（A）=saf（A）cic（A），wlp（An，Q） = Nat·wlp（An，Q）.trm（A）的定义可以根据以下事实来理解：这里存在两种不同的不终止风险：第一，A的任何特定执行可能不会终止;第二，重复本身可能是永久的，这也会表现为非终止。当A是安全的时，我们可以避免第一种风险，而当A事实上，A可以被证明是抽象命令表达式的Egli-Milner最小固定点X（A; X）[] skip.它是我们定义迭代的基础杜内118⇒⇒¬⇒||||||||iteration：采用熟悉的形式，而GdoA end，其中G是谓词，A是抽象命令。其定义为：而G do A end= （G =A）;<$G =skip。对迄今为止一直被认为是基本编程结构的东西进行如此巧妙的解构但是，尽管我们已经使用了我们建设性地定义的抽象命令重复闭合，但阿布里亚尔使用了他所谓的广义替换的传递开，在定义中，他不得不求助于固定点理论。G=skip充当了一个选择过滤器：它约束执行它前面的重复闭包的恶魔选择G=的任何有限重复 A（如果存在的话，只能有一个）是可行的， G错误。相反，如果G=A的每一次有限重复都使G为真，那么恶魔必须选择永久的重复，如果这是可行的，那么迭代当然，如果无休止的重复是不可行的从上面的定义可以很容易地证明，while true doskip end =从不这证明了我们之前对never作为无限循环的抽象规范的操作解释是正确的并行组合：采用A B的形式，其中A和B是抽象命令。执行继续进行，直到A和B都终止，结果，如果有的话，是A和B的合成结果。这里，不直接指定wlp（A B，），而是指定prd（A B）。像往常一样，帧合并，所以我们有框架（A||B）=frame（A）frame（B），trm（A||B）=trm（A）trm（B），prd（A ||B）=prd（A）prd（B）。我们的平行合成是相当普遍的：它如果它们的框架不相交，则表示A和B的独立执行。这篇论文草稿的一位审稿人对trm（A B）的上述定义表示了一些疑虑，因为正如他所说，但我们的并行运算符实际上只不过是[17]的并行合并的一个特殊情况，引用Hoare和He的话杜内119||¬每个进程首先在其私有版本的共享变量上独立执行当所有这些都终止时，它们对共享变量的更新被合并并写回共享变量的全局版本在我们的例子中，这种合并是两组结果的直接可行融合[2]当A和B对一个共同变量的各自效应完全不可调和时，A B是不可行的。我们在[6]中定义了一个类似的平行合成，用于广义替换。我们这里的定义实际上比那个定义简单，因为完全正确性导致了广义替换的trm和prd之间的依赖性，这在一般正确性中没有反映出来，其中trm和prd彼此独立。concert：采用A#B的形式，其中A和B是抽象命令。它表示A和B在终止契约中各自帧的不相交副本上的并行执行这些协调一致的处决继续进行，直到任何一方终止。如果有的话，总体结果完全取决于谁终止了。它们的帧是合并的，所以我们有frame（A #B） = frame（A）frame（B），trm（A #B）=trm（A）trm（B），wlp（A#B，Q）=wlp（A，Q）wlp（B，Q）。我们可以想象concert在Unix/C环境中的具体实现，父进程派生两个子进程，然后等待其中一个终止，然后杀死另一个。因此，concert给我们提供了一种方法，可以将一个可判定的规范细化为一对并行执行的半可判定程序。我们将在下一节用一个家庭寓言来说明这一点13丢失的戒指假设我们在家里丢了一枚贵重的戒指，不是在花园里就是在家里。设A为“找到丢失的戒指”的指定设P为谓词然后P=A是指定P|P=A这相当于半可判定的规范杜内120过程会找到它，但如果没有，它规定了一个永无止境的花园搜索。相应地，欧元/英镑|P =A相当于半可判定的具体化“搜索房子寻找丢失的戒指”。如果我们有一个熟悉花园的园丁和一个熟悉房子的管家，这两个搜索很容易单独实现。但我们注意到，它们必须同时执行。我们知道，我们的管家和园丁将各自不知疲倦地寻找，从不承认失败。因此，它很可能是徒劳的，例如，首先要求管家进行她的房子搜索，并等待其结果，然后再决定是否要求园丁进行他的花园搜索。因为管家的搜索可能永远不会有任何结果，因为只要她找不到戒指，我们可以证明，对于任何抽象命令A和任何谓词P，A= （P|P=A）#（<$P| <$P =<$A）这证明了我们的并发搜索策略作为实现我们的总体搜索要求的手段的有效性事实上，如果没有人熟悉房屋和花园的私密地理，这可能是唯一可行的14音乐会的单调性也许，concert是我们最典型的抽象命令构造函数。但是，人们可能会合理地问，它真的那么特别吗？毕竟，难道我们不能用一点独创性在广义替换的完全正确世界中定义一个类比算子吗？例如，trm（S）trm（T）|（trm（S）=S [] trm（T）=T）？Doesn’t this express the behaviour of generalised substitutions 也许令人惊讶的是，答案是肯定的：它确实表达了一种替代，这种替代总是像S和T中的任何一个保证在它们中的一个结束时结束一样。这似乎表达了两个并行程序合作的思想，因此无论哪一个程序被保证完成，都定义了整个计算的结果。那么，为什么答案很简单，这个构造函数就像纳尔逊... 因此，它对于分段程序开发是无用杜内121相比之下，concert就像我们所有其他抽象命令结构一样，具有关于一般正确性精化的单调性的基本属性因此，它可以用于分段程序开发。这是关于一般正确性的关键点在它的上下文中，我们可以定义可用的新运算符，如concert，即使它们在完全正确性上是可定义的，但最终在那里是无法实现的。15结论我们已经比较了程序语义的总正确性和一般正确性的治疗，认为后者是一个适当的基础，为许多今天的计算需求，他们的口音的互动性我们已经提出了我们的抽象命令语言，来自Abrial由于在B方法中，广义替换总是在抽象机器的上下文中解释，其状态变量预计提供有效的框架上下文，Abrial我们的抽象命令语言的一个重要特征是它对框架的明确和完全组合的处理，这符合摩根的具体化陈述的精神[21]。这有助于精确和严格地描述语言的各种构造器的框架扩展或框架收缩效应。我们的抽象命令语言的所有构造器对于抽象命令的细化都是单调的，因此该语言提供了一个统一的自包含系统，用于逐步和分段算法开发，以将抽象规范的一般正确性转化为可执行实现。我们知道没有其他的规范语言为这样的开发提供了可比较的上下文;因此，我们相信，我们的抽象命令语言是一个原创性的贡献，它将促进抽象规范在一般正确性方面的表达，以及它随后对实现的细化。引用[1] Abrial，J.- R.，“The B-Book: Assigning Programs to Meanings,”Cambridge University Press,[2] 回来，河。和M. Butler，Fusion and simultaneous execution in the refinementcalculus，Acta Informatica35（1998），pp. 921-940[3] Dijkstra，E.，[4] Dijkstra，E.和C.Scholten，杜内122[5] Dunne，S.，在一般正确性技术报告。计算与数学学院，提赛德大学，2000年。[6] Dunne，S.，安全机器：B，in：J的新规范构造。阿荣，J. Woodcock和J.Davies，editors，FM472-489[7] Dunne ， S. ， W. Stoddart 和 A.Galloway ， 将 广 义 替 代 扩 展 ， 在 ： H 。Habrias，editor，The First B Conference（1996），iSBN 2-906082-25-2.[8] Dunne，S.， W. Stoddart和A. Galloway，Specification and Refinement inGeneral Correctness ， in ： A. 埃 文 斯 ， D. Duke 和 A. Clark ， editors ，Proceedings of the 3rd Northern Formal Methods Workshop （ 1998 ） ，http://www.ewic.org.uk/ewic/workshop/view.cfm/NFM-98.[9] 弗洛伊德河，《应用数学专题讨论会论文集》（Proceedings of Symposia inApplied Mathematics19，1967年），第19页。十九比三十二[10] Gries，D.，“The Science of Programming,” Springer-Verlag,[11] 海耶斯一、分离 定时 和 计算 在 实时 细化，在：J. Grundy，M. Schwenke和T. Vickers，editors，International RefinementWorkshop and Formal Methods Pacific 1998（1998），pp.1-16号。[12] 海斯岛，推理非终止循环使用期限命令，在：R. Backhouse和J. Oliveira，编辑，程序构造数学（MPC 2000），2000，也可 作 为 技 术 报 告 UQ-SVRC-00-02 ， www.example.com 获 得http://svrc.it.uq.edu.au。[13] Hehner，E.，终止是定时，在：J. van de Snepscheut，编辑，程序构造的数学，计算机科学讲义（1989年）第375号，pp.36比47[14] Hehner，E.，“A Practical Theory of Programming,” Springer-Verlag,[15] Hehner，E.和A. Gravell，Refinement semantics and loop rules，in：J.Wing，J. Woodcock和J.Davies，editors，FM1497-1510年。[16] Hoare， C. ， 编 程 理 论 ： 自 上而 下 和 自 下 而 上 以 及 会 议J. Wing， J.Woodcock and J. Davies，editors，FM'99-FormalMethods，number1708inLectureNotesinComputerScience（1999），pp. 1-27号。[17] 霍尔角和H.Jifeng，[18] 雅各布斯，D。和D. Gries，General correctness：a unification of partial andtotal correctness，Acta Informatica22（1985），pp. 67比83[19] 琼斯角，澳-地“使用VDM的系统软件开发（第2版）”，Prentice- Hall，1990年。杜内123[20] 摩根，C.，ACM Transactions on Programming Languages andSystems10（1988）.[21] 摩根，C.，“Programming from Specifications (2nd edn),” Prentice HallInternational,[22] 纳尔逊，G.，Dijkstra演算的一般化[23] Spivey，J.，“The Z Notation: a Reference Manual (2nd edn),” PrenticeHall International,