紧耦合系统的组合性：命题类型解释的统一风格时间逻辑标记下的形式验证规则

理论计算机科学电子笔记159（2006）299-323www.elsevier.com/locate/entcs紧密耦合系统的组合性：命题类型解释马克-奥利弗·施特尔SRI International，计算机科学实验室333Ravenswood Avenue，Menlo Park，CA 94025，USAstehr@csl.sri.com摘要复杂软件系统的设计从根本上依赖于对抽象组件及其交互的理解。尽管作曲技巧在实践中得到了成功的运用，但这种技巧的使用往往是非正式的和直观的，存在对组合系统的正确行为的判断，但没有明确表示。 在本文中，我们将展示将这些司法机构视为一等公民所能获得的好处。 本文的相当一般的设置是一个正式的发展的统一风格的时间逻辑标记的过渡系统的演算的归纳结构，已进行了使用Coq证明助理在形式上严格的方式。我们的发展不仅包含了最初的UNITY方法来进行程序验证，以及最近的New UNITY方法，而且在几个重要方面超越了它，例如程序/系统模型的通用性，公平性的概念以及组合性的问题。最后一个方面，我们认为是至关重要的软件工程的基础，是本文的主题。我们提出了一个一般的证明规则，在紧耦合系统中的活性断言的组合验证。它依赖于组合证明的概念，而组合证明又与并行程序的无干扰证明的经典工作密切相关。这个新的证明规则的公式化及其可靠性的验证不仅利用了归纳构造演算强大的归纳推理能力，而且还以一种基本的方式使用了命题作为类型的解释和相关的证明作为对象的解释。保留字：UNITY，程序验证，组合性，软件工程1介绍随着当今软件系统的高度复杂性1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.073300M.- O. Stehr/Electronic Notes in Theoretical Computer Science 159（2006）299可以被构造为一组相互作用的组件，这些组件的复杂性非常小，可以单独理解。软件工程的一个重要目标是在许多其他约束下找到这样的分解，例如可测试性，可重用性和协作开发的便利性，仅举几例。然而，不仅是组合本身，而且组件和组合系统行为的正确性也是软件工程活动的重要产物。这些有价值的信息通常存在于非正式和直观的层面，但通常不明确，因此无法与其他团队成员沟通，甚至可能丢失，通常会导致系统设计中的细微错误。我们认为，软件工程的基础不仅应该解决组件的精确描述，它们的接口，以及它们的行为属性，而且还需要包括一个明确的语言来传达这些属性的合理性。在本文中，我们使用一个完全正式的方法来研究什么可以通过提供这些信息。为了解释我们的想法，我们使用了著名的UNITY方法的推广，这是Hoare断言方法对程序验证的自然扩展UNITY方法是由Chandy和Misra在80年代后期开发的[5]。 它的形式化技术包括编程语言和时态逻辑。程序被看作是无限的不确定迭代变换，而具体化语言是线性时间时态逻辑的一个变体。今天，UNITY是一种众所周知的方法，在许多案例研究中，它为（组合）系统验证提供了一种令人惊讶的优雅技术。UNITY和密切相关的形式主义的应用可以在[5，27，28，7，44，17，42，6，41，25，13，29，38，12，23]中找到，包括并行程序的规范，设计和验证，分布式算法和协议，异步硬件和移动系统。本文的基础是我们使用Coq证明开发系统[3]在归纳构造演算（CIC）中对UNITY时态逻辑的推广的形式化开发[43]。与大多数现有的UNITY形式化相反，我们遵循最近的New UNITY [27，28]建议(New)UNITY提出了一些关于程序概念和公平性概念的有趣的概括，这为处理与UNITY编程语言非常不同的系统规范语言提供了基础，例如Petri网的不同描述[38]和基于重写的形式主义，例如重写逻辑[24]。在形式方面，我们的治疗受益于M.- O. Stehr/Electronic Notes in Theoretical Computer Science 159（2006）299301类型理论的几种应用这个最有趣的结果是使用类型论的活性断言，这是本文的主要主题的一个新的组合定理。 我们认为，可以毫不夸张地说，这个结果在CIC中被公式化和证明的形式优雅是通过命题作为类型及其相关的证明作为对象的解释而成为可能的。据我们所知，这是迄今为止尚未考虑的这种解释概况. 在第2节中对（新）UNITY的一个健全而完整的片段进行了简短的非正式介绍之后，我们在第3节中提出了我们对UNITY的正式概括，然后在第5节中进一步扩展，我们的组合性结果。在第4节中，我们验证了一个简单而著名的UNITY示例，该示例将在第6节中重复使用，以说明我们的结果的应用。2一个完整的统一的声音片段我们首先对最初的UNITY方法进行非正式和简单的概述。正如在[5]中所解释的，UNITY编程语言是一种类型化语言，程序由：（1）程序变量及其类型的，以及（2）一组有限的条件多重赋值语句。1UNITY程序的语义是一种交错语义：状态是一种类型良好的变量赋值。与最初的UNITY方法不同，它要求程序在满足初始化条件的状态下启动，这是程序的固定部分，我们省略了初始化条件，并使用以下更自由的语义。2.执行序列是一个无限状态序列，它从任意状态开始，通过对语句的公平和非确定性UNITY中的公平性意味着每个语句都被无限频繁地执行。它也被称为无条件公平，因为报表的条件不被考虑在内。UNITY方法基于一个简单的时态逻辑，它只包含几个时态运算符，称为STABLE、INVARIANT、UNLESS、ENSURE和LEADS。这些是一元或二元运算符，在状态谓词上制定断言，即取决于系统状态的谓词。虽然1由于技术原因，所有UNITY程序都被假定包含skip，一个没有任何效果的语句[27]。[2]不幸的是，[5]中形式上的不一致导致了对UNITY断言含义的一些混淆。这个问题和可能的解决方案在[26，35，39，36，37，18，16，13]中讨论。我们的简单解决方案允许执行序列以任意状态开始的动机可以在[43]中找到302M.- O. Stehr/Electronic Notes in Theoretical Computer Science 159（2006）299UNITY时态逻辑应该被归类为线性时间时态逻辑的一个变体，有一些有趣的特性使得不可能根据标准线性时间逻辑定义它的所有运算符[22]。我们的形式化发展受到了[27，28]中一个更近期的UNITY逻辑表示的启发除了[5]中的基本运算符UNLESS和ENSURE之外，我们遵循新UNITY方法引入了两个新的运算符CO和TRANSIENT，因为它们为定义其他运算符提供了更基本的基础。在下文中，我们给出了一个简短的非正式的时序逻辑的执行语义方面的概述。然而，当我们在下一节中为转换系统引入UNITY风格的时态逻辑时，我们将按照[5]的精神直接根据系统定义时态断言。这种方法的优点不仅在于它的数学优雅，而且还具有相当程度的语义独立性。下面的四个时态断言，实际上可以被认为是线性时间时态逻辑的一个片段，是提升到执行序列集合的各个执行序列的属性。(1)pCOq：3如果p在任意状态下成立，那么q在后继状态下成立。 (2)STABLEp：一旦p成立，它就保持为真。(3)pUNLESSq：如果p成立，那么至少只要q不成立，p就(4)p导致q：如果p成立，那么q最终会变为真。4此外，还有两种不同类型的辅助算子，它们通常不会在高级规范中使用。 相反，它们被用作辅助断言，以在验证阶段建立指向断言的线索(1)瞬时p：p不能永久成立，因为一旦p为真，就有一个单一的陈述将其证伪。(2)p确保q：p，除非q，如果p成立，那么q最终会为真，因为只有一个语句伪，伪。除了到目前为止介绍的时态运算符之外，我们还使用了两个ad-这是一种断言：ind. 不变断言和不变断言。 它们都依赖于一个额外的状态谓词IC，称为初始化条件，它通常指定一组在特定上下文中被认为是初始的状态：（1）IND。不变ICp：IC蕴含p和稳定p。(2)不变ICp：p在从满足IC的某个状态可达的每个状态中成立。很明显，每个归纳不变量都是不变量。反之则不成立，因为不变式只是关于可达状态的断言，3 读作[4]这包括q保持不变而没有任何延迟的情况。 我们总是在这个意义上使用M.- O. Stehr/Electronic Notes in Theoretical Computer Science 159（2006）299303并不意味着任意状态的稳定性。因此，（非归纳）不变量一般允许我们避免对程序行为的过度指定。另一方面，非归纳不变量对于组合推理不太有用，因为可达状态的集合在组合下一般不鲁棒。归纳不变量是合成的，因为它们是关于任意状态的断言。因此，这两种不变量在实践中都是需要的。关于这些问题及其与UNITY替换公理的关系的澄清性讨论可以在[16]中找到3通用UNITY在本节中，我们将UNITY形式化地推广到标记转移系统。UNITY程序可以被视为迁移系统的一个特例，如下所示：程序的每个条件多重赋值语句都被视为一个动作。关联的转换关系采用描述语句对状态的影响的函数的形式。如果UNITY语句的条件未满足，则启用相应的操作，但操作的结果是状态上的身份关系。因此，使能性谓词在UNITY程序的这种转换系统表示中得到了平凡的满足。在本文的其余部分，我们以经典的方式使用CIC的逻辑论域Prop，也就是说，我们假设经典公理，如排中律，逻辑可拓性和证明无关性，这些都在适当的经典集合论解释下得到满足。另一方面，universeType将用作通用数据类型的universe。3.1标签转换系统在下文中，我们在抽象标记转移系统的设置下工作，该抽象标记转移系统由状态的类型st、动作的类型act和三元转移关系transs给出。给定一个动作e和状态s，s变量st：类型。变量行为：类型。变量transs：act->st->st->Prop。我们还需要视图的概念，它只是一组操作。一个视图导致了一个对预设转换系统的限制，所有的时态断言都是相对于一个视图定义的。为了简洁起见，我们经常在非正式的解释中确定一个视图及其诱导的转换系统。304M.- O. Stehr/Electronic Notes in Theoretical Computer Science 159（2006）299定义视图：=（集合行为）。除了转移系统，我们假设一个弱公平行动组的集合wf这个集合的意义将在3.4节中解释。变量wf：（set（set act））。3.2状态谓词和函数我们有一个s_prop类型的状态谓词，即依赖于状态的命题。定义s_prop：= st-> Prop。通常的逻辑运算符和量化器以自然的方式从Prop提升到s_prop它们由s_true、s_false、s_or、 s_and、 s_imp、s_iff、s_not、s_ex和s_all表示。一个例外是处处运算符，它不产生一个状态谓词，而是一个（状态独立的）命题。定义无处不在：= [p：s_prop]（s：st）（p s）。3.3安全性声明我们从合作者的定义开始回想一下，对于两个谓词p和q，断言（coEpq）意味着如果p在某个状态下成立，那么q在E中的每个可能的后继状态下都成立，不管发生什么动作定义hoare：= [e：act][p，q：s_prop]（（s，定义co：= [E：view][p，q：s_prop]（e：act）（In actE e）->（hoare e pq）.随后，我们根据co定义了更多的算子。记住，断言（除非E p q）声明在E中，p成立，除非q成立，或者更准确地说，如果p在某个状态下成立而q不成立，那么在下一步p保持为真或q变为真。进步不是强制的，即断言不排除p永远为真而q永远不成立的可能性定义unless：= [E：view][p，q：s_prop]（coE（s_and p（s_not q））（s_orp q））.断言（stableEp）断言p是稳定的，即一旦p在E中为真，它就继续保持。定义稳定：= [E：view][p：s_prop]（coE p p）。更强的断言（ind_invariantE ICp）指出p是Ew.r.t.中的归纳不变量。 初始化条件IC。除了p的稳定性之外，还要求p由IC暗示。定义ind_invariant：=[E：view][IC：s_prop][p：s_prop]M.- O. Stehr/Electronic Notes in Theoretical Computer Science 159（2006）299305（everywhere（s_imp IC p））/\（stableE p）.我们还介绍了断言的形式（不变E ICp），其中指出，p是隐含的一些归纳不变Ew.r.t.初始化条件IC。定义不变式：=[E：view][IC：s_prop][p：s_prop](ExT[inv：s_prop]（ind_invariantE IC inv）/\（everywhere（s_imp invp）。最后，我们有状态谓词（siE IC），称为最强不变量[20]，它表征了可达状态集。定义si：=[E：view][IC：s_prop][s：st]（p：s_prop）（ind_invariant E IC p）->（p s）.3.4活性断言最初的UNITY逻辑可以表达导致断言，一类特殊的活性断言，声明如果某个条件在某个点成立，那么最终将达到某个（其他）条件。独立于UNITY，导致断言对于并发程序验证的相关性已经在[19]中指出。 在我们看来，UNITY方法的一个重要贡献可以在断言和时态逻辑观点（关于安全性和活性断言）的紧密集成中找到，–与安全断言（非平凡）相反，活性断言只有在系统满足一定的公平性要求时才能被证明正如在New UNITY中一样，活性断言确保和leads_to构建在unless和transient断言之上，公平性的概念优雅地封装在transient操作符中。我们将这个运算符从无条件公平性推广到弱公平性，如下所示：断言（瞬时p）意味着p不能永久保持，因为一旦它为真，它最终会由于单个弱公平行为组而被证伪为了表达这种进步的要求，我们引入了sco，一个强版的co，它考虑到了使能性我们首先将动作e的使能性定义为状态谓词（enablede）这对于动作e可能发生的那些状态s是满足的定义启用：= [e：act][s：st]（ExT（[s'：st]（transe ss'）））。然后，我们将（enabled e）提升到动作组，从而产生另一个状态谓词（group_enabled E），如果组E（即该组中的至少一个动作）被启用，则该状态谓词（group_enabled E）被满足。306M.- O. Stehr/Electronic Notes in Theoretical Computer Science 159（2006）299定义group_enabled：=[E：（set act）][s：st]（ExT[e：act]（In act E e）/\（enabledes））。断言（scoE pq）不仅意味着在E中满足p的状态的后继状态是满足q的状态，而且它还声明被视为一组动作的E在每个满足p的状态中被使能。定义en：= [E：（set act）][p：s_prop]（everywhere（s_imp p（group_enabledE）。定义sco：= [E：（set act）][p，q：s_prop]（en E p）/\（co E p q）。对于下面的瞬态定义，我们假设一个弱公平行为群的集合wf，它是除了转移系统之外指定的。为了使的定义尽可能简单，我们采用这样的约定：空群总是弱公平的，因此包含在wf中。5现在，如果给定的视图E包括弱公平的动作组E'，使得对于满足p的每个状态，通过执行来自E'的动作而获得的每个后继状态使p无效，则断言（瞬态Ep）被满足定义瞬态：= [E：view][p：s_prop]（ExT [（在（集合动作）wfE'）/\（包含动作E'E）/\（scoE'p（s_notp）。确保断言基本上是，除非配备了活性。为了确保活性，我们只需要添加（transientE（s_and p（s_notq），表示（s_and p（s_notq））不能在E中永久保持。这就排除了p永远成立而q永远不为真的可能性。定义确保：=[E：view][p，q：s_prop]（除非E pq）/\（瞬态E（s_andp（s_not q）。随后，我们使用[5]中的标准归纳定义来引入LEADSTO作为主要运算符来表达活性断言。leads_to算子是在ensure之上归纳定义的，它是满足leads_to_basis、leads_to_transitivity和leads_to_dis三个性质的最小预测交界处。 记住，断言（leads_toE p q）应该包含6，如果p在E中的任意状态下成立，那么q最终将在未来成立。这显然是由（确保E p q）暗示的，证明了下面归纳定义中的含义leads_to_basis此外，传递性是5新UNITY假设每个程序都包含一个没有任何结果的skip由于我们的惯例，我们在这里不需要相应的假设[6]请注意，我们在这里只陈述了一个含义。虽然UNITY时态逻辑是完备的[31，32]，正如我们在第2节中介绍的那样，我们还没有研究我们的推广的完备性问题M.- O. Stehr/Electronic Notes in Theoretical Computer Science 159（2006）299307显然，这是leads_to的一个属性，正如隐含式leads_to_transi- tivity所要求的那样。最后，蕴涵leads_to_disjunction形式化了一个析取性质：如果断言（leads_toE（Pi）q）对状态谓词族P成立，那么我们可以得出（leads_to E（s_ex T P）q）。 证明很简单：给定一个满足析取（s_ex T P）的状态s，必须有某个索引i使得（P i）在s处为真。 然后我们可以使用前提（leads_toE（Pi）q）来推断q最终将成立。感应式leads_to [E：view]： s_prop->s_prop->Prop：=leads_to_basis：（p，q：s_prop）（确保Ep q）->（导致_到Ep q）| leads_to_transitivity：（p，q，r：s_prop）（leads_toEp q）->（leads_toEqr）->（leads_toEp r）| leads_to_disjunction：（T：Type）（P：T->s_prop）（q：s_prop）（（i：T）（leads_toE（Pi）q））->（leads_toE（s_exT P）q）。3.5基本成分在整个文件中，我们是在一个单一的过渡系统，它代表了整个系统的全局视图的背景下工作，我们认为这个系统的组件作为特定的本地视图。自然合成操作是这些视图的简单联合，即，集合的并集UNITY风格的时态逻辑的一个显著特征是，几乎所有的操作符都具有基本的组合属性。最重要的几项如下。定理联合：（E，(co（Union actEE '）p q）。定理stable_union：（E，（stable（Union actE定理indinv_stable_union：（E，E '：view）（IC：s_prop）（p：s_prop）（ind_invariant E IC p）->（stable E' p）->（ind_invariant（Union act E E '）IC p）.定理unless_union：（E，（除非（欧盟法案EE '） p q）。定理unless_stable_union：（E，（除非（欧盟法案EE '） p q）。定理transient_union：（E，E'：view）（p：s_prop）（（transient E p）\/（transient E'p））->（transient（Union act E E'）p）.308M.- O. Stehr/Electronic Notes in Theoretical Computer Science 159（2006）299定理确保_unless_union：（E，（确保（欧盟法案EE'）pq）。定理确保_稳定_联合：（E，（确保（欧盟法案EE'）pq）。值得注意的是，唯一不享有类似于上述组合规则的运算符是不变的，并导致_to。幸运的是，invariant有一个组合对应项ind_invariant，但leads_to缺乏简单的组合规则显然不能令人满意。然而，对于具有不受限制的组合概念的紧耦合系统，正如我们在这里使用的那样，由 于 组 件 之 间 可 能 的 干 扰 ， 我 们 似 乎 不 能 期 望 类 似 于ensure_unless_union的规则4说明性示例在本节中，我们简要回顾了众所周知的常见会议时间问题及其在一个简单的UNITY程序中的解决方案[5，28]。这个例子将在后面重复使用，以演示我们的组合验证方法。用自然数对时间进行建模，问题是找到两个人最早可能的共同会面时间。我 们 假定存在这样一个共同的见面时间，并且对于两个人中的每一个人，我们分别假定一个函数，比如f和g，使得f（t）和g（t）是不早于t的最早的可用时间。 我们正在寻找一个程序， 一个可变的时间，并满足以下时间规范：（1）部分正确性，即时间近似于共同的会议，即它永远不会减少，永远不会超过最小的共同会议时间。（2）共计正确性，即除了部分正确性之外，时间最终将包含最小的公共相遇时间。UNITY程序给出了满足这种非正式规范的解决方案：程序CMT声明时间：nat初始时间 =0指定时间：= f（time）|time：= g（time）end4.1形式化非正式的问题说明意味着我们可以假设两个函数f和g的自然数是递增和单调的。77谓词le和lt表示自然数上的标准全序≤和 nat。公理f_is_ascending：（m：nat）（le m（fm））. 公理g_is_ascending：（m：nat）（le m（g m））.公理f_is_monotone：（m，n：nat）（le m n）->（le（f m）（f n））.公理g_is_monotone：（m，n：nat）（le m n）->（le（g m）（g n））.一个公共的会面时间被形式化为f和g的公共定点。常见定义：=[t：nat]（f t）==t/\（g t）==t。接下来，我们假设存在一个最小的公共会议时间，我们用cmt表示，正如我们的非正式规范所述。变量cmt： nat.公理cmt_exists：（common cmt）。公理cmt_smallest：（m：nat）（common m）->（le cmt m）.将UNITY程序CMT表示为带标签的转换系统使用了两个动作update_f和update_g，这两个动作对应于程序的两个状态。为了简洁起见，我们省略了这种直接表示的细节4.2部分正确性我们的总体策略是首先证明部分正确性的安全断言，然后在这些安全断言之上，建立完全正确性所需的活性断言。这两个主要定理将完全对应于我们前面给出的非正式说明。我们的证明与[28]中给出的证明类似，但所有步骤都使用Coq进行了机械检查。所有相关的证明规则都列在附录A和B中，以供参考。我们从一个引理开始，说明如果时间有一个值m，那么在每个后继状态下，时间不会增加到（fm）以上，或者不会增加到（g m）以上。证明是通过展开co，然后验证动作update_f和update_g的断言来完成的。引理CMT_S1：（m：nat）（coCMT（[s：st]（（stime）== m））([s：st]（le（s time）（f m））\/（le（s time）（gm）。下一个引理CMT_S2是通过对程序变量time应用消去定理（参见附录B）获得的。 为此，我们在定理消除中通过时间分别实例化x、p和q，[s ： st] （ common n）-> （ le（ s time） n）和[m ：nat][s ：st]（le（ stime）（fm））\/（le（s time）（g m））。 其 余 的共同前提由引理CMT_S1精确给出。引理CMT_S2：（n：nat）(coCMT[s：st]（（common n）->（le（stime）n））（s_ex？[m：nat][s：st]（（common n）->（lemn））/\310M.- O. Stehr/Electronic Notes in Theoretical Computer Science 159（2006）299((le（s time）（f m））\/（le（s time）（g m）。下一个引理指出，时间，这是提前的程序，不能跳过任何共同的会议时间。证明从前面引理的共同断言开始，并使用右侧弱化来获得稳定断言。引理CMT_S3：（n：nat）（稳定CMT（[s：st]（commonn）->（le（stime）n）。由于（[s：st]（common n）->（le（stime）n）最初成立，即它由[s：st]（stime）== O实现，我们可以建立归纳不变量。引理CMT_S4：（n：nat）(ind_invariant CMT[s：st]（（s time）== O）（[s：st]（common n）->（le（s time）n）。用cmt代替n，我们得到定理CMT_S5，该定理确立了以下事实：时间不能增加到超过最小公共会议时间CMT。定理CMT_S5：（ind_invariant CMT[s：st]（s time）==O [s：st]（le（s time）cmt））.最后，我们证明了定理CMT_S6，说明时间只能增加而不能减少。证明是通过展开co，然后分别使用公理f_is_ascending和g_is_ascending考虑两个动作update_f和update_g中的每一个来完成定理CMT_S6：（m：nat）（co CMT [s：st]（m ==（s时间））[s：st]（le m（s时间）。4.3完全正确性为了建立完全正确性，我们必须证明活性断言，即如果程序在满足初始化条件的状态下启动，最终会达到最小公共会议时间cmt。形式上，我们希望证明：（leads_toCMT（[s：st]（（s time）==O））（[s：st]（（stime）==cmt）为此，我们根据定理leads_to_rev_nat_induction（见附录A）对自然数进行（逆向）归纳。我们必须提供一个变量，它增加到某个最大值。一个明显的选择是变量time的值，以及最小的公共会议时间cmt作为其最大值。定义变量：= [s：st]（s时间）。下面我们需要下面的引理CMT_S7，这是从引理CMT_S3通过用cmt实例化n而得到的特殊情况。引理CMT_S7：（稳定CMT [s：st]（le（变体s）cmt））。M.- O. Stehr/Electronic Notes in Theoretical Computer Science 159（2006）299311下面我们准备应用逆向归纳法则线索to_rev_nat_induction，稍后将用于证明引理CMT_L13，这反过来又直接暗示了最终活性属性CMT_L14。在引理CMT_L12中直接证明了逆归纳规则的前提中的leads_to断言，作为确保断言。我们首先证明这个确保断言的安全性部分，这是引理CMT_S8中给出的除非断言：如果时间没有超过cmt，那么下一个状态只有两种可能性：要么我们到达cmt，要么时间增加但不超过cmt。证明展开，除非并将co_stable_conjunction应用于CMT_S7和CMT_S6。然后利用共蕴涵方法得到目标。引理CMT_S8：（m：nat）（除非 CMT（s_and[s：st]（le（s time）cmt）[s：st]（m==（s时间））（s_or（s_and [s：st]（le（s time）cmt））[s：st]（ltm （s time）[s：st]（（stime）== cmt）。上述的活动性部分确保断言将由引理CMT_L11中的瞬时断言提供，这又将通过中间引理CMT_L9从下面的引理CMT_L10证明，该中间引理陈述：如果时间不是公共的相遇时间，则时间最终将改变。引理CMT_L9：（m：nat）（瞬态 CMT[s：st]（not（common（s time）/\（m ==（s time）。证 明是 通过 展开 瞬 态 和 区分 两种 情况 来完 成的 ： 如果 m等 于（fm），则update_g负责进度，否则update_f是进度的见证。利用transient_implications和cmt是最小公共相遇时间的事实，我们得到引理CMT_L10。引理CMT_L10：（m：nat）（瞬态CMT[s：st]（（lt（s time）cmt）/I（m ==（s time）。transient_implications的另一个应用加上一些时间上的案例分析最终产生CMT_L11，这正是我们证明引理CMT_L12所需要的。引理CMT_L11：（m：nat）（瞬态 CMT（s_and（s_and [s：st]（le（s time）cmt））[s：st]（m==（s时间））（s_not（s_or（s_and [s：st]（le（s time）cmt））[s：st]（lt m（stime））[s：st]（（stime）== cmt）。现在我们可以结合安全性（引理CMT_S8）和活性（引理CMT_L11）312M.- O. Stehr/Electronic Notes in Theoretical Computer Science 159（2006）299断言以获得确保断言，该断言可以直接用于通过leads_to_basis证明以下引理（参见leads_to的归纳定义）。引理CMT_L12：（m：nat）（leads_to CMT（s_and[s：st]（le（s time）cmt）[s：st]（m==（变量s））（s_or（s_and[s：st]（le（stime）cmt）[s：st]（ltm （变式））[s：st]（（stime）== cmt）。最后， 我们可以使用逆向归纳规则 leads_to_rev_nat_induction来证明CMT_L13。 我们通过cmt实例化maximum，并按照上面的定义逐个变量地实例化。leads_to前提是CMT_L12。 引理CMT_L13指出，如果时间没有超过最小的会议时间cmt，那么它将在未来的某个时候达到cmt。引理CMT_L13：（leads_to CMT([s：st]（le（s time）cmt））（[s：st]（（s time）== cmt）。当然，leads_to的左边特别涵盖了我们原始程序的初始化条件。因 此 ，我们通过使用leads_to_implications削弱左侧来获得最终的活性结果CMT_L14。定理CMT_L14：（导致 CMT([s：st]（（stime）== O））（ [s：st]（（stime）= = cmt）。同时，定理CMT_S5、CMT_S6和CMT_L14证明了在非正式规范中制定的程序的完全5通过命题作为类型的我们希望，通过前面的例子，我们已经使读者相信，即使是对一个表面上简单的程序的验证，如果以一种形式上严格的方式进行，也需要大量的计算。因此，对于交互式验证技术的实际应用来说，重用组件及其证明是绝对必要的虽然我们对大多数时态算子有简单的复合性定理，但对于leads_to没有类似形式的对应定理。特别地，我们不能在定理ensure_unless_union中仅仅用leads_to替换ensure。让我们仔细看看这个问题：假设我们有组件E和E'以及状态谓词p和q，使得（leads_to E p q）和（除非E' p q）成立。那么我们一般不能推断（leads_to（UnionactEE'）pq）成立，因为组件E可能在从p到q的执行路径上干扰E'，例如：通过修改E的进程所依赖的变量显然，这样的干扰可以导致新的执行可能性，而不会导致q。并行程序中的干扰问题是一个众所周知的问题，M.- O. Stehr/Electronic Notes in Theoretical Computer Science 159（2006）299313[30]中提出的解决方案（也参见教科书介绍[2]）基于无干扰证明方案的概念。这个概念在本质上是丰富的细节它涉及到一个用证明注释的程序的概念，这似乎很难用形式逻辑来表示。在这一节中，我们建议使用类型论本身根据命题作为类型/证明作为对象的解释所提出的抽象概念来获得标记转换系统的一般上下文中的完全令人满意的无干扰形式化。在命题作为类型的解释[15]（也见[9]）下，也称为公式作为类型的类比，逻辑公式A被解释为类型[A]]，使得A是可证明的，如果[A]被居住。一个证明P被解释为一个对象[P]]，使得[[P]是[A]的元素]。这第二部分被称为证明作为对象的解释或证明作为程序的解释。类型论中逻辑的这些解释最初用于Curry-Howard同构[15]的背景中，这需要更强的对应性，即逻辑中证明的规范化对应于类型论中的规范化。命题作为类型的解释也可以被看作是BHK解释的类型论具体化[14]，Brouwer，Heyting和Kolmogorov已经使用它来解释直觉主义逻辑的含义。Curry-Howard同构已经在直觉逻辑和相应的类型理论的背景下被成功地建立，例如在高阶直觉逻辑和构造演算之间[10]。回想一下，在我们的形式化中，我们以经典的方式使用CIC的逻辑论域Prop以及标准的证明无关性公理。由于我们现在感兴趣的是将证明视为时态逻辑的leads_to片段的信息对象，而不是假设证明不相关，因此我们将相关部分移到论域类型，并利用命题作为类型解释所提供的视图的二重性，即，我们同时使用传统的类型视图作为数据类型和逻辑视图作为公式。换句话说，我们现在将同时处理两种不同的逻辑：（1）不谓词逻辑，它存在于标准命题论域Prop中，被公理化为具有证明无关性的经典外延逻辑;（2）由类型论域层次提供的谓词逻辑，它是直觉的、内涵的，并且认真对待证明。第一步是通过将Prop替换为Type，从无信息的leads_to断言迁移到有信息的inf_leads_to断言。我们得到以下定义：感应inf_leads_to [E：view]： s_prop->s_prop->Type：=inf_leads_to_basis：（p，q：s_prop）（确保Ep q）->（inf_leads_toE p q）314M.- O. Stehr/Electronic Notes in Theoretical Computer Science 159（2006）299| inf_leads_to_transitivity：（p，q，r：s_prop）（inf_leads_toEp q）->（inf_leads_toEqr）->（inf_leads_toEp r）| inf_leads_to_disjunction：（T：Type）（P：T->s_prop）（q：s_prop）（（i：T）（inf_leads_toE（Pi）q）->(inf_leads_toE（s_exT P）q）。我们已经正式验证了，如果我们将leads_to替换为inf_leads_to，那么到目前为止我们开发中的所有证明仍然有效。这是一个事实的结果，即相对于逻辑的基础片段，UNITY的leads_to片段已经以完全建设性的方式新定义的主要目的是给断言（inf_leads_toE pq）除了它们的逻辑解