Java ITP：基于Hoare逻辑和代数语义的验证工具

理论计算机科学电子笔记176（2007）29-46www.elsevier.com/locate/entcsJava+ITP：基于Hoare逻辑和代数语义的验证工具1RalfSasseandJos'eMeseguer2伊利诺伊大学厄巴纳-香槟分校计算机科学系厄巴纳，IL 61801，美国摘要Java+ITP是一个实验工具，用于验证Java语言的顺序命令子集的属性。它是基于一个代数延续传递风格（CPS）的语义，这个片段作为一个等式理论在Maude。它支持组合推理的霍尔逻辑这个Java片段，我们提出并证明正确的代数语义。在被分解之后，Hoare三元组被转换成语义上等价的一阶验证条件（VC），然后将其发送到Maude's Inductive Theorem Prover（ITP）这个项目的长期目标是使用可扩展和模块化的重写逻辑语义的编程语言，CPS公理化确实是非常有用的，开发类似的可扩展和模块化的霍尔逻辑通用程序验证工具可以基于。关键词：代数语义;霍尔逻辑;程序验证; Java1介绍这项工作是一个更广泛的研究项目的一部分，即重写逻辑语义学项目，许多作者正在为该项目做出贡献（见最近的调查[19，18]和参考文献）。总体目标是使用编程语言的重写逻辑语义定义，包括并发语言，以及像Maude这样的语言来生成有效的语言实现，包括解释器和编译器，以及这些语言的复杂程序分析工具，包括无限状态程序的不变检查器，模型检查器和定理证明器。所有这些工具的吸引人的特征之一是它们的通用性：通过利用公共的底层语义和最大化语言定义的模块化，通常可以使用通用的基础设施以通用的方式为不同的语言生成程序分析工具，但具有竞争力的性能。1 这项研究得到了ONR Grant N 00014 -02-1-0715的支持。2 电子邮件：{rsasse，meseguer} @ cs.uiuc.edu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.06.00630R. Sasse，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）29在解释器，不变检查器和模型检查器的情况下，这已经在许多语言中得到了证明，包括Java和JVM的大子集（参见[19，18]对不同语言案例研究的详细讨论）。对于定理证明者来说，情况没有那么先进。一个未解决的和令人兴奋的研究问题是找到霍尔风格的通用和模块化程序逻辑[12]，在重写逻辑语义的基础上对这些逻辑进行数学证明，并开发通用定理证明技术来支持不同语言中的程序逻辑推理。我们还没到那一步。事实上，我们认为实现这一雄心勃勃的目标的一个合理方法是通过案例研究收集经验证据，以帮助我们找到这种通用和模块化程序逻辑的轮廓。本文在这个方向上取得了一些进展，专注于一个子集的顺序Java。具体而言，我们：(i) 通过向[7]中给出的Java大片段添加额外的功能，使其适合于定理证明目的，从而使基于Maude的延续传递风格（CPS）重写逻辑语义学适应于[ 7 ]中给出的Java大片段。虽然我们目前关注的是一个适度的顺序片段，但在Java和其他语言中有足够的证据（参见[19，18]中的讨论），支持基于CPS的重写逻辑定义是模块化和可扩展的主张;因此，我们相信我们目前的工作将自然扩展到Java和其他语言中更雄心勃勃的语言片段。(ii) 为这个片段开发一个Hoare逻辑，并根据CPS语义从数学上证明我们的Hoare规则的正确性。即使对于这个适度的片段，这也是不平凡的，因为一些标准的Hoare规则，包括条件和for while循环的规则，实际上是无效的，必须适当地推广才能适用于Java程序。(iii) 开发这种霍尔逻辑的机械化，支持：（i）使用霍尔规则进行组合推理，将霍尔三元组分解为更简单的三元组;（ii）生成一阶验证条件（VC）;以及（iii）使用底 层 CPS 语 义 ， 通 过 Maude 的 归 纳 定 理 证 明 器 （ ITP ） [ 4 ] 释 放 此 类VCJava+ITP是作为Maude的ITP的扩展而开发的虽然Java+ITP主要是一个研究工具，以帮助我们推进基于模块化重写逻辑语义定义开发程序的泛型逻辑和泛型程序验证器的长期目标，但我们也发现它作为伊利诺伊大学厄巴纳-香槟分校的教学工具它已被学生广泛用于程序验证（CS 476）的研究生课程，并将在今年冬天用于形式方法研究生课程（CS 477）。Java+ITP的概念基础正是人们对任何基于语言重写逻辑语义的定理证明工具的期望。如前所述，我们的Java片段的CPS语义在Maude中是公理化的由于我们目前关注的是一个连续的片段，这就定义了一个方程理论R. Sasse，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）2931JAVAX.因此，该语言我们使用这个数学模型TJAVAX来证明我们的霍尔规则的语义。类似地，与霍尔三元组相关联的一阶VC则是被初始模型TJAVAX声称满足的归纳目标，并且Maude因此，对于这个片段，我们在众所周知的代数语义框架内[10];然而，在包括线程和并发的未来扩展中，语义将由重写理论给出，并且归纳推理将基于这种重写理论的初始模型在Java逻辑、语义和定理证明工具方面有大量的相关工作，例如[16，14，13，15，9，20，17，2，3]。我们在第6节中讨论了相关的工作;我们还讨论了与我们更接近的工作，例如Maude ITP [4]，我们的工具基于此，ASIP-ITP工具[6，22]，当然还有JavaFAN项目[7，8]，这项工作在定理证明层面上做出了贡献。本文的其余部分组织如下。我们的Java片段的CPS语义在第2节中进行了总结。基于语言的初始代数语义的Hoare三元组的一阶语义在第3节中解释。我们的霍尔逻辑及其证明将在第4节中讨论。在Java+ITP工具中，这种逻辑的机械化及其在示例中的使用将在第5节中讨论。第6节介绍相关工作和结论。相关的技术报告[24]包含了循环规则正确性的数学证明，以及两个Java程序的证明脚本。2顺序Java子集我们提出了我们所选择的Java子集的语义的一些亮点。由于篇幅限制，我们没有展示整个语法、状态基础结构和实际语义。然而，整个定义可以在网上找到[23]。我们感兴趣的Java片段包括算术表达式、赋值、顺序组合和循环。我们的语义使用连续传递风格（CPS）的方法。这样做的好处是使我们的语义定义易于扩展，以适应未来更多的Java功能。例如，异常，对象，多线程和所有其他Java特性都可以使用CPS风格表示，如[7]中的原型版本所示。我们的规范在风格上类似于[7]中更大Java子集的原型解释器，但有一些差异/优化，利用了我们所选子集的顺序特性。我们说明我们的语义明确其状态基础设施，并显示了一些选定的功能的语法和语义。2.1Java的国家基础设施为了能够描述Java的语义，我们必须指定程序的执行如何影响状态基础结构，它包含程序变量的值和其他状态信息。国家基础设施由以下模块定义，我们分别指定位置，环境，价值观，32R. Sasse，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）29构成国家的商店和延续。程序变量不会直接映射到其值，而是映射到一个位置店内这导致了变量到位置和位置到值的两级映射。 LOCATION模块定义了什么是位置，例如位置为l（17）。 它还展示了如何将多个位置连接在一起，我们通常处理表达式列表等。fmod LOCATION正在保护INT。排序Location LocationList。子排序Location LocationList.op _，_：LocationList LocationList -> LocationList [aslogid：noLoc]. op 1：Nat -> Location.endfmENVIRONMENT模块将环境定义为从名称到位置的有限映射它导入NAME模块，该模块定义名称、名称列表和名称的相等性。fmod环境保护位置。保护名称。排序环境op noEnv：-> Env.op [_，_]：名称位置->环境op：Env Env->Env[aslogid：noEnv]。变量X Y：名称。vars Env：环境varsL L '：Location. var Xl：NameList. var Ll：LocationList.op _[_<-_]：环境名称列表位置列表->环境op _[_<-_]：环境名称位置->环境eq Env[（）<- noLoc] = Env.等式Env[X，Y， ValueList。op _，_：ValueList ValueList -> ValueList [aslogid：noVal]. op [_]：ValueList -> Value。endfmfmod STORE正在保护位置。延伸价值。sort Store.op noStore：-> Store。op [_，_]：Location Value -> Store.op ：StoreStore -> Store [ascurrentid：noStore]。endfm对于这种语言来说，环境和商店是以非常具体的方式定义的。使用更抽象的环境/存储概念将具有以下优点：R. Sasse，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）2933程序验证的观点，如[6，22]中所示，对于一种非常简单的语言。但是一个更抽象的环境/商店概念并不能很好地处理我们语言中可能存在的副作用和隐藏，为此我们选择了具体的变体此外，这将使将来更容易 相反，更抽象的状态定义不允许显式存储更复杂的信息，如异常、循环或锁信息在我们接下来定义的延续中，所有的执行上下文都被存储。这可以被视为需要执行的“程序的其余部分”。这里显示的两个操作符是执行的两个不同的结束点。 在语义中，我们将根据需要定义其他具有共域延续的运算符。例如，每一个Exp排序的表达式都可以放在顶部（即，在前面）一个延续。fmod CONTINUATION是一个连续的排序。操作停止：->继续。opres：-> Continuation.endfm状态由状态属性组成，这些属性是环境、存储、输出和下一个空闲内存位置的计数器，每个属性都由某个操作符包装。它的结构是由通常的结合交换多集并算子得到的一组这样的属性。fmod STATE是对ENVIRONMENT的扩展。扩展商店延续延续。排序StateAttribute MyState。子排序StateAttribute MyState。op_，_：MyState MyState-> MyState [aslogid：empty]. 操作：Env-> StateAttribute。op n：Nat ->StateAttribute。op m：Store-> StateAttribute。opout：Output -> StateAttribute。对SuperState WrappedState进行排序。子排序WrappedState WrappedState。操作状态：MyState ->WrappedState。op k：Continuation -> SuperState。op _，_：WrappedState-> WrappedState [aslogid：noState]。op_，_：SuperState SuperState-> SuperState [aslogid：noState]。endfm需要第二组排序声明（以及相应的运算符），因为我们不需要上下文，即 ， 继 续 ， 成 为 国家的一 部 分， 但 只 能 与 之 组 合 。 所 以 ， 不 是 有e（..），m（..），n（..），k（..）我们现在有状态（e（..），m（..），n（..）），k（..）.由于这种结构，我们可以通过简单地检查状态的排序来检查程序的终止如果它是超级状态的排序，仍然有一些contination-uation，因此代码，左和程序尚未终止。 如果结果状态是一个WrappedState，我们就知道所有的代码都已经执行了。对空延续发生了什么的定义需要支持这一点，并且确实如此。34R. Sasse，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）292.2一些特征我们感兴趣的Java片段包括算术表达式、赋值、顺序组合和循环。现在让我们来看看Java子集的一些特性我们首先讨论加法，然后是条件和最终循环。的增订条文加法的句法是利用类属表达式的定义来定义的，它主要是介绍表达式的不同可能形式。fmodARM-EXP-SYNTAX是ex GENERIC-EXP-SYNTAX。op _+_：Exp Exp-> Exp [prec 40 gather（E e）]。...在ARPEN-EXP-SEMANTICS中定义的运算符+->允许我们计算位于延续之上的加法表达式。第一个等式将E + E第二个等式通过将计算表达式得到的两个整数相加并将结果放在延续堆栈的顶部来计算->+fmodARP-EXP-SEMANTICS保护ARP-EXP-SYNTAX。扩展了Generic-EXP-SEMANTICS。op + -> _：Continuation -> Continuation。变量E E '：var K：继续。varsI I '：Int.等式k（（E + E ' ） -> K ） = k （ （ E ， E' ） -> + ->K ）。等式k（（int（I），int（I '））-> + -> K）= k（int（I + I'）-> K）。...如果...在Java中，If-Then-Else结构实际上并不包含then，而是具有IF-SYNTAX中指定的语法，该语法导入语句，这是一种不同于表达式的结构，因为它不创建返回值。以其人之道，解析优先级时，悬空的else问题在Java语言规范[ 11 ]中得到了解决，也就是说，else部分属于最里面的if。我们认为If-Then是语法糖，因此在IF-SYNTAX中给出一个等式，将其转换为我们的If-Then-Else，这意味着我们不需要为它费心在语义学上。 此外，一个方程对于这种脱糖是足够的。fmodIF-SYNTAX是ex STATEMENT-SYNTAX。来自GENERIC-EXP-SYNTAX。op ifelse_：Exp Statement Statement -> Statement [prec 110].op if：Exp Statement -> Statement [prec 115].变量E：失效日期var St：语句。eq ifE St =ifE St else;.endfm一个条件语句的求值被分为两部分：首先对条件求值，同时冻结continuation中的两个代码部分，然后，一旦条件求值为true或false，选择正确的路径。注意，我们需要在这里导入布尔表达式fmod IF-SEMANTICS是ex IF-SYNTAX。从通用-经验-语义学。从语句语义学。来自BEXP-SEMANTICS。OP？（_，_）->_：语句语句继续->继续。变量E：失效日期vars St St '：声明。var K：继续。等式k（（ifEStelse （St，S t ' ） - > K ） 。等式k（bool（true）->？(St，S t' ） - >K ） =k （ S t- >K ） 。eq k（bool（false）->？(St，St '）-> K）= k（St'-> K）。endfmR. Sasse，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）2935While循环。while循环的语法很简单。注意，while的第二个参数是一个语句，但是我们总是可以通过使用花括号将几个语句的顺序组合包装到一个块中，例如。{S1 S2}，带S1S2声明 一个块又被算作一个语句。fmodWHILE-SYNTAX是ex STATEMENT-SYNTAX。来自GENERIC-EXP-SYNTAX。操作while：Exp语句->语句[prec 110]。endfm定义循环的语义现在非常容易，通过使用条件的语义并一步一步地展开循环：fmod WHILE-SEMANTICS是ex WHILE-SYNTAX。从通用-经验-语义学。从语句语义学。来自IF-SEMANTICS。变量E：失效日期var St：语句。var K：继续。等式k（（whileE St）->K）= k（E->？({St而E（St），;）-> K）。endfm2.3Java子集完整的函数定义给出了一个精确的数学公理化，实际上是我们选择的Java子集的初始代数语义，对于推理和程序验证来说是足够的。但是由于语义方程是基础连续的，所以上述语义方程也给这个Java子集提供了操作语义实际上，我们可以通过从左到右的代数简化方程来描述语言的执行。因此，我们的语言定义在本质上给了我们一个语言的解释者。请注意，在一些次要的方面，我们并不遵循Java的严格语法，因为Maude的一些内置类型。例如，程序变量是用Maude引用标识符建模的，因此前面总是有一个引号（操作符#i（），以避免Maude内置的INT模块中的操作Java 中的 算 术 运 算。 使 用initial，我 们 创 建 了一 个 初 始 的空 s tate 。Byadding'|CODE是一个简单的语句，当CODE是一个简单的块语句的代码片段时，我们可以计算在给定状态下执行该代码片段所产生的状态。此外，STATE[VAR]返回状态STATE中变量VAR的值。实现这一点的等式是：op _[_]：WrappedState Name-> Value。var MYS：MyState. var X：Name. var L：位置。var Env：环境var V：值。var M：存储。eq状态（（MYS，e（[X，L] Env），m（[L，V] M）[X] = V。以下是一些示例红色（初始|（int'x = #i（1）; int 'y = #i（20）;'x = #i（300）; } 'x= 'x + 'y ;））红色（初始|（int'x = #i（1）; int 'y = #i（20）;{int'x = #i（300）; } 'x = 'x + 'y ;））}'x].回程rewrites：86in10 ms cpu（10 ms real）（8600rewrites/second）结果值：int（320）分别地，由于块中对“x”的赋值的阴影36R. Sasse，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）29rewrites：86in0 ms cpu（0 ms real）（~rewrites/second）结果值：int（21）一个简单的swap例子，其中swap只是一个由等式swap =（int'T = 'X ; 'X = 'Y ; 'Y= 'T ;）定义的程序的简写符号红色（初始|（int'X=#i（7）;int'Y=#i（5）;swap））红色（初始|（int'X=#i（7）;int'Y=#i（5）;swap）一个小的阶乘程序红色（初始|（int<'n = #i（5）; int 'c = #i（0）; int 'x = #i（1）; while（' c 'n）{ 'c = 'c + #i（1）;'x = 'x * 'c ; }））' x].计算5的阶乘，并返回：rewrites：416in0 ms cpu（0 ms real）（~rewrites/second）结果值：int（120）3霍尔三重3.1前和后条件回想一下我们在第二节中展示的交换程序2.3. 当在等式设置中完成时，该示例程序的正确性规范可以如下所示：（int“X ;”int“Y ;）|（swap））'X] =（ctxState（（int 'X ; 'int 'Y ;））'Y]（int“X ;”int“Y ;）|（swap））'Y] =（ctxState（（int 'X ; 'int 'Y ;））'X]我们能够验证这一点，只使用我们的语义方程和莫德的内置方程简化现在用S代替ctxState（（int（I：Int）（J：Int）（S）（S）|（swap））'X] = int（I）（S|（swap））int（J）在这里，我们有一个隐含的前提条件，即我们从一个状态开始，和我们称这个方程为（S）假设在程序执行之前保持，即前提条件。注意，该方程在每个方程中具有状态变量S的单次出现，并且可以被认为是状态谓词，具有整数变量I和J作为参数。考虑上述公式，（S|（swap））'X] = int（I）（S|（swap））int（J）R. Sasse，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）29371n它应该在程序执行后保持不变。这也可以被看作是一个状态谓词，即状态谓词（t）（S）不适用于S，而是适用于状态S|（交换）执行后。我们称之为（†）后置条件。注意，它还有整数变量I和J作为额外的参数。状态谓词。这个例子提出了状态谓词的一般概念，直观地说，它是一种持有或不持有状态的属性，可能与一些额外的数据参数有关。因为在我们的Java子集中，唯一的数据是整数，所以这样的参数必须是整数变量。因此，对于我们的语言，我们可以将状态谓词定义为方程的合取t1= tJ. tn=tJ在模块JAVAX中，使得方程中的所有项中的变量的集合V具有最多一个State类变量S，其可能出现不止一次，并且其余变量都是Int类变量。当然，我们可以进一步推广，允许一个任意的一阶公式（变量V有相同的条件），而不仅仅是一个方程的合取此外，这个概念自然地扩展到其他顺序语言，这些语言可能具有除整数之外的其他数据结构。然而，在实践中，上述概念是相当普遍的;除其他外，因为使用等式定义的等式谓词，我们可以将任意的布尔方程组合（因此任何无量化器的公式）表示为单个方程。3.2霍尔三重上面我们对交换的指定的例子是通过Hoare三元组（在C.A.R.之后）指定顺序命令程序p的属性的一般方法的范例。（见[12]），{A}p{B}其中A和B是状态谓词，分别称为前提条件，三元组的后置条件在这种表示法中，互换的规范被重新表述为，{（S）给定我们对命令式程序的语义的代数方法，这完全是一个由我们的语言的初始模型，即初始代数TJAVAX满足的一个初始化或初始化的优先级。的38R. Sasse，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）29模块JAVAX是定义Java子集语义的模块。它导入所有其他模块，定义语法，状态基础设施和语义。因此，我们通过等价性定义程序p关于Hoare三元组的部分正确性TJAVAX|={A}p{B}优惠TJAVAX|=（V）A（（S |p）：WrappedState）（B（S/S|（p））。这里的：表示排序成员资格，这反过来又表示程序在状态S下启动时终止。注意，在部分正确性解释中，终止条件位于蕴涵的左侧因此，我们的交换示例变为TJAVAX|=（I：Int）（J：Int）（S：State）（S）'Y] = int（I）（S）'X] = int（J）（S）|swap）：WrappedState（S）|（swap））'X] = int（I）（S|（swap））int（J）.这只是我们最初的正确性条件加上排序要求的终止条件当然，因为swap是一个终止程序，所以在这种情况下这是超级复杂的，但是当涉及到循环时就不是超级复杂的了。4Java子集的Hoare逻辑及其判定霍尔的一个重要贡献是提出了他的三元组作为一个组成逻辑的程序，通过收集推理规则的基础上结构的程序文本分解证明的正确性更复杂的程序证明为简单的子程序。然而，霍尔逻辑是依赖于语言的：一个霍尔规则在一种给定的语言中对一个结构有效，在另一种语言中可能是无效的。例如，经典的Hoare条件规则和for循环规则即使在我们简单的Java片段中也是无效的因此，重要的是：（i）选择Hoare规则，以充分捕捉特定语言中的给定特征;（ii）在数学上证明这种规则的正确性。对于这第二个目的，有一个精确的数学语义的语言问题是一个基本的先决条件。因此，我们引入了霍尔逻辑为我们的Java子集，并证明其规则的正确性，我们的JAVAX形式语义的基础上例如，为了证明序列复合p q的正确性，他给出了规则，{A}p{B}{B}q{C}{A}p q{C}通过分析语义方程和三元组的语义，可以很容易地为我们的Java子集进行R. Sasse，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）2939在我们的Java语义中，另一个容易判断的规则是跳过程序.{A};{A}对于条件句，我们需要更努力地工作，因为经典的条件句霍尔规则是无效的。关键的困难是评估条件的布尔表达式可能会 这里，evalTst（S，TE）给出布尔值，测试数据的平均值将在状态序列中出现。 我们的任务是|'我们可以将测试表达式的“执行”与程序的其余部分分开。现在我们已经没有了|的方法是将一个数据和一个预记录片段进行合并，并且还将一个状态和一个表达式进行合并，但是由于所涉及的不同类型，因此不会产生歧义，这不是一个问题。此外，由于在霍尔三元组中，我们有时需要考虑表达式对于仅与语句执行相结合的副执行目的，我们的Hoare三元组不仅允许语句，还允许表达式。任何使用|允许以“ad-hoc”重载方式使用符号。请注意，这样的“组合”虽然在状态上的效果方面有意义，但并不对应于合法的Java程序;然而，它们在Hoare规则中是需要的。当然，这两种用法|是密切相关的，因为，例如，给定一个状态，s、表达式e和语句p，我们从语义上解释e的结果|p在s上的方程S|（e）|p）=（s| e）、|p.不可能使用通常的Java程序连接这里因为测试表达式与其他语句的类型不同。但使用|运算符，它可以首先被评估，这样它的边对象就改变了状态，然后结果被丢弃，执行照常继续。这是我们允许表达式像语句一样使用的方式，只是为了它的副作用。函数evalTst将给定状态下的测试表达式计算为布尔值。由于在某些规则中多次写出这个值有点麻烦，我们稍微重载了我们的符号，并在下面以两种不同的方式使用测试t。在Hoare三元组的属性部分中，t将代表等式evalTst（S，t）=true，其中S是用于区分状态的变量，该方法必须保持不变，并且类似地，对于evalTst（S，t）=fals e，该方法将被设定。t的使用（分别是它的否定）只给了我们布尔值，而不是改变国家。当状态S不明显时，我们将回到evalTst符号。我们使用tin的另一种方式是像往常一样在代码部分中（在if或while构造中），或者只是为了上面描述的可能的状态更改。t的不同用法在我们的条件句霍尔规则中得到了说明，{A}t|p{B}{At}t|q{B}{A}if tp else q{B}这捕获了if的通常语义，就像在更简单的语言中一样，但是在contrasthere，sincetcannhavesidee t e te|在执行过程中40R. Sasse，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）29条件句的两个分支在各自的情况下。 是不够要知道t的计算结果是真还是假，这是两个属性所保证的，但是t也需要为它可能的副作用而执行。这个霍尔规则仍然简化了事情，因为我们现在不必根据测试值，但我们只需要执行测试表达式。我们也可 以 为 您 提 供 一 个 均 衡 的 组 合 规则，|我也是由于存在副作用，因此必须执行xtrae或rre另一个非常有用的规则，基于霍尔三元组的语义的简单判断，是后果规则，A A1{A1}p{B1}B1B{A}p{B}我们的语言子集中最重要的规则是while循环部分正确性的证明规则。这里我们面临着与条件语句相同的问题，因为循环条件也可以有副作用。它采取的形式，{A}t|p{A}{A<$t}t{A<$t}{A}whiletp{A<$t}这一规则需要一个更复杂的证明，这在技术报告[24]中给出的证明中完成。状态谓词A称为循环的不变量该规则需要额外的Hoare三元组进行测试：（q） {A<$t}t{A<$t}这是因为侧效应可以随着环路展开而传播。一个循环是这样工作的：当t p →t|p|当t p →... →不|p|......这是什么？|p|当t p→t|p|......这是什么？|...|p|不|t在这样达到的最终状态中，测试t不一定会被评估为假。在最终状态之前的状态中，它确实评估为假，但它的副作用可能导致它的下一个评估再次为真。为了防止这种情况，必须将Hoare三元组（q）添加到循环规则的证明义务出现此问题的Java程序示例如下：int（（ ' i=' i+# i （ 1 ） ） = =# i （ 1 ） ） .在这里，条件检查但是如果条件在这个最终状态下被评估，所以这里的条件在最终状态下不是假的。一个阶乘的例子。考虑2.3节中的阶乘程序。为了证明它的正确性，即正确计算阶乘函数，我们首先需要定义R. Sasse，J.Meseguer/Electronic Notes in Theoretical Computer Science 176（2007）2941在数学上，这样的函数，通过定义运算符facValue及其定义方程，op facValue：Int-> Int.var I：Int.ceq facValue（I）= 1 if 0

下载后可阅读完整内容，剩余1页未读，立即下载