保持一致性的一致性增强算法理论及其应用

网址：http://www.elsevier.nl/locate/entcs/volume61.html20页基于保持一致性的一致性增强算法理论约束Sebastian Link，Klaus-DieterScheweMassey大学信息系统系Private Bag 11222，Palmerston North，NZ [s.linkjk.d.schewe]@massey.ac.nz摘要一致性实施为形式规范语言中的通用验证技术提供了一种替代理论。 我们以保护命令的形式考虑规范。 其基本思想是用一个程序规范S的最大一致性特化（GCS）SI来代替它，它对于给定的静态约束I是可证明一致的，根据特化顺序保持S的效果，并且是具有这些性质的最大值。该理论已被证明提供了几个优势。特别是，一个庞大的类复杂的speci阳离子的增强过程可以减少到它的基本组件。而且，该结果可以顺序地得到，并且与给定约束的顺序无关。此外，算术逻辑已被用来表明，GCS可以有效地计算一个合理的大类的程序规范和不变式。然而，所有的结果已经取得了关于潜在的特殊化秩序。这种简单的顺序揭示了一些明显的弱点。在本文中，我们展示了如何专业化的顺序可以取代的概念，限制。一个程序规范S的特殊化等价于保持S的底层状态空间上的所有约束。 因此，这使我们能够削弱专业化秩序，以保持某些特定的约束。我们定义NE最大一致性约束条件（MCES），表明这些是密切相关的GCSs和证明MCES可以顺序和独立地从一组给定的静态约束的顺序这支持了MCE的概念导致一致性执行的定制理论的猜想。关键词：形式规格说明，保护命令，算术逻辑，约束，一致性，GCS，MCEc 2002年由Elsevier Science B出版。诉 在CC BY-NC-ND许可下开放访问。21介绍形式规范语言的一个共同特征是静态约束。他们的目的是限制法律国家的集合。主要的问题是保证一致性。如果程序规范S在满足静态约束I的状态中开始，那么我们期望S也在验证I的状态中终止。有几种方法可以保证一致性，例如在运行时进行一致性检查或在编译时进行一致性验证。检查和验证都不允许对程序进行更改。它们要么是一致的，因此被接受，要么不被接受。也没有反馈给设计者如何改变程序以实现一致性。一致性强制旨在为所有这些方法提供一种替代方案。一般来说，执行的目的是系统地修改程序，使结果保持一致。文[6，7，8]中的方法要求修改后的程序规范是原程序规范关于某个偏序v的最大一致缩减。 如果我们给定一个程序规范S和一个不变量I，我们正在寻找一个新的程序规范S I，它与I一致，满足S I v S，并且具有这些性质。结果 SI称为S关于I的最大一致特化（GCS）。偏序背后的意图是保留效应，即，只要Tv S成立，由于S引起的状态变化就应该保持为T引起的状态变化。程序规范语义等价类偏序的GCS选择是操作专门化。出发点是考虑由给定程序规范S约束的状态变量。对于这些状态变量，特化Tv S只允许已经出现在S中的执行。然而，不受S约束的状态变量可以任意处理。利用Dijkstra和Nelson[5]风格的谓词Transformer语义，可以很容易地将操作专门化形式化。在[7]中详细研究了最大一致特化SI。 除了存在性和唯一性（直到语义等价），还有两个重要的结果。第一个是交换性结果，表明GCSSI1^^In 可以被建立顺序地采取一个ny阶的不变量I i。这反过来又只是集中在一个不变量。第二个结果涉及组合性。 使用[5]中的保护命令，我们可以从简单的程序规范构建复杂的程序规范。最简单的规范是通过赋值和一些常数如skip给出的。 一般来说，替换非常简单的规格是不够的 在S区的昏迷指数结果将不是GCSSI。然而，在一些温和的技术限制下，我们得到至少一个推广的GCS，和GCS本身的结果添加一个先决条件。（S;I） 7的可计算性文献[2，3]中研究了S I及其有效性。3除了非常一般的情况下，它可以表明，类的程序规范和不变量，它是公正地谈论一个计算方法，是相当大的。因此，GCS方法是一种理论上有充分依据的一致性实施方法。如果我们将自己限制在GCS的确定性分支上，该方法也可以实现运行时方法。在这种情况下，只需要考虑转让的顺序，这允许忽略技术和可计算性限制。第二节简要回顾了GCS算法的研究成果尽管GCS方法在理论上很有优势，但从实用的角度来看，它是有争议的。对状态变量的改变不受原始程序规范的约束，允许太多的自由，而该方法对其他状态变量的限制可能太大一个想法，以削弱保留顺序考虑的一组transi- tion不变的满足，由原来的程序规范。它们被称为“非对称”。 由于操作专业化等价于在只求解由S所引起的状态变量时保留S的所有约束条件，因此简单的思想是保留一组不同的约束条件。 这导致了最大一致性效应器（MCE）的定义。非正式地，MCE作为稍微扩展的程序规范的GCS而出现，但是不再需要考虑被检测的状态变量的集合在第3节中，我们将引入极大一致的概念，无论如何，表明它们涵盖了合理的例子，并且它们与GCSs密切相关。我们将在第4节中进一步讨论。我们认为，一个天真的reformulation的交换性的结果将失败的MCE框架内。尽管如此，我们证明了一个足够的版本，允许执行MCE顺序，也独立于给定的一组不变量的顺序最后，我们指出，最大一致性预服务器的方法已经与数据库中的原始框架相关联理论（见[4]）。2最大一致专业化为了发展一致性实施理论，我们采用基于状态的方法来进行形式规范。这意味着我们明确地支持状态和状态转换的概念。程序规范将采用Nelson [5]定义的扩展保护命令的形式。语义将由定义在算术逻辑[1]之上的谓词转换器表示，如[2，3]中所示。42.1程序规格算术方法[3]旨在将一致性强制与经典递归理论联系起来。因此，采用具有固定结构（N; 0; S;+;;=）的一阶逻辑L，称为算术逻辑。在此，非负整数N定义域，0; S; +;和=以通常的方式解释。然后，我们将这种解释推广到项T和公式F。 如果V表示变量的集合，那么解释被一个函数捕获：V！N，或者甚至由它在项或公式中的自由变量x i上的值（x i）。也就是说，我们可以写一个k元组，知道自由变量的数量是k。定义2.1状态空间是L ar的变量的集合X。X=fx1; ：;xk g上的状态是一个函数：X！ n= n， （x 1）;：; （x k））2 N k.2静态约束是可以在状态中计算的公式。这使我们能够区分法律状态，即，满足约束条件的国家和非合法国家。定义2.2我们定义状态空间X上的一个静态不变量（简称：X-约束或X-公式）为Lar的公式I，其中X中有自由变量（fr（I）X）。2接下来，我们在给定的状态空间上定义一个程序规范定义2.3设X是一个状态空间。受保护命令的语言包括skip、fail、l o op、simultaneousassignme ntxi1：=ti1 k： kxik：=tik2S（X）对于状态变量xij 2X和术语tij 2T，序列组成S1;S2，选择S12S2，限制选择S1S2，后卫P！带X的S-公式P，无限选择@yS和变量y，最小 定点S：f（S），带有保护命令表达式f（S）=P！ T;S2：P！ skip，其中程序变量S不在T内出现。2请注意，包含受限制的选择运算符要以保持正交性。更深层次的解释见[5]。此外，我们只考虑简单WHILE循环形式的递归为了在算术逻辑的基础上定义受保护命令的语义，我们将S两个预处理指令转换器wlp（S）和wp（S）联系起来|也就是说，从公式（等价类）到公式（等价类）的函数|具有标准的非正式含义：wlp（S）（“）c表征那些初始状态，使得每次终止S的执行都导致满足”的状态。Wp（S）（“）c表征那些初始状态，使得S的每次执行开始于终止并导致满足”的状态。记法wlp（S）（'）和wlp（S）（'）对应于S的通常弱（自由）条件与弱条件'. 为了定义一个空间，我们经常使用符号w（l）p（S）（'）来表示两个谓词5变形金刚一次 如果这发生在一个等价物中，那么省略括号中的每一个- thing就得到了wp-部分，而仅仅省略括号就得到了wlp-部分。 给定这一点，我们定义了一个对偶谓词变换w（l）p（S）byw（l）p（S）（“），：w（l）p（S）（：”）。现在考虑以下用于我们的保护命令语言的谓词转换器的定义（为了说明，请参见[2，3]）w（l）p（skip）（'），'w（l）p（fail）（'），truew（l）p（loop）（'），false（_true）w（l）p（xi1：=ti1k： kxik：=tik）（'），fxi1=ti1; ：;xik=tikg：'w（l）p（S1;S2）（'），w（l）p（S1）（w（l）p（S2）（'））w（l）p（S12S2）（'），w（l）p（S1）（'）^w（l）p（S2）（'）w（l）p（S1S2）（'），w（l）p（S1）（'）^（wp（S1）（true）_w（l）p（S2）（'））w（l）p（@xjS）（'），8xj：w（l）p（S）（'）w（l）p（P！S）（'），P）w（l）p（S）（'）：关于w（l）p（S：f（S））（'）的定义，请参见[3，第3节]。 我们说 ， S 是 一 个 X- 命 令 ， 对 于 某 个 状 态 空 间 Xw （ 1 ） p （ S ）（“），”对于每个m∈Y-都成立“，其中X\Y=1，并且X是最小的。2.2一致性和全球控制系统我们想推导出一个证明义务，它描述了程序规范S与静态约束I的一致性（见[3]）。定义2.4设S是一个程序规范，I是一个静态约束，两者都在X上.则S关于I是相容的（简称：I-consistent）i I）wlp（S）（I）成立。2操作专门化旨在减少现有的执行，同时扩展状态空间，并允许对新的状态变量进行任意的额外更改[3]。定义2.5设S和T是X和Y上的程序规范，其中XY。 则S由T（TvS）iw（l）p（S）（'）p（l）p（T）（'）确定.26我们注意到，对于wp部分，要求wp（S）（true））wp（T）（true）成立就足够了。操作专门化定义了程序规范语义等价类上的偏序v，使失败最少一致性的证明义务和操作特殊化的定义足以确定该方法的中心概念。定义2.6设S为Y命令，I为X上的约束，其中Y为X.S关于I的最大一致特化（GCS）是X-7我我X我我命令SI与SIvS，使得SI关于I是一致的，并且每个I一致的特化Tv S满足TvSI。2第一个重要的结果涉及交换性，即，关于合取的GCS可以使用任何约束顺序连续构建命题2.7对于两个约束I和J，我们总是得到I^J！SI^J 我^J！ （SI）J a resemanti canallyequivalent.2如果为一个复杂的程序规范S构建GCS只需要用它们的GCS替换S中的基本操作，那就太好了。设S0表示这种朴素的语法替换的结果但总体而言0 不是昏迷指数它甚至可能不是S的特化，也可能是一个一致的专业化，但不是最大的。存在一个技术条件，这意味着至少S I vS0 保持。相应的结果在[3]中称为上界定理。我们需要一个确定性分支S+的概念，阳离子S，其要求S +vS，wp（S）（真），wp（S+）（真）和wp（S+）（'）wp（S+）（'）对所有'成立。这里，最后一个条件表示S+确实是确定性的，即，当verj= （; ）（x;y）时，则j=：0（x）并且当verj=（;1）时， （x;y）和j=（;2） （x;y）保持，然后1（x）=2（x）。总之，S的决定性的branchS+是决定性的，S的tic特化，当且仅当S包含执行。转换约束是一种减少允许的转换对集合的方法定义2.8状态空间X上的转移约束是公式J，其中X[X 0]中的自由变量使用X的不相交系数X0，即， fr（J）X[X0. 2我们将新的约束定义为由一个特定的约束满足的转换约束，阳离子。 为了建立一个空间，我们使用fx=x0 g来表示关于状态变量的非空集合的 替 换 。定义2.9设S是X上的一个程序集。S的转移约束是X上的转移约束J，满足f0= xg：wlp（S0）（J），其中S0通过将所有xi重命名为x0而由S得到.2例2.10看一个新元组t插入到关系r中的插入S，即，Sr：=r[ft g. 然后，对于M而言，以下是对于S的约束条件：t 2 r 08u：u2r）u2r08u：u2q，u2q0对所有关系s chemataq6=r和8u：u6=t^u2r0）u2r.2我们写'来表示状态的特征公式。S8令XY1=fy1; ：;ymg，Y1=fx1; ：;xl g，并假设fx0; ：;x0g定义2.11设S =S1;S2为Y -命令，使得Si为Yi的Yi-命令Y（i = 1;2）. 设我是X约束和Y约束X.1L91我我我是Y的一个不相交的拷贝，也与X不相交。 则S是I-约化形式i我如果它是S +的n-约束，则它也是S+;S2的n-约束.如果它是S +的n-约束，则它也是S+;S2的n-约束.2对于S1的每个确定性分支S+，以下两个条件{其中00 0x=（x1;：;xl），x=（x1;：;xl）{保持：所有国家其中j=：我我们有，如果'）fx=x0g：（8y* 是， （一）A1所有国家其中j=我们有，如果1）fx=x0g：（8y* 是， *一）是一个1 1非正式地，I-约化是序列S1;S2的一个性质，它排除了在S1的任何分支内错误地导致强制执行的临时状态的出现，但这与整个规范无关将此定义扩展到序列以外的任意命令是很简单的。上界定理已经有了一个复合性的主张，但它还没有给出GCS。上的主要定理的思想GCS是从S切出 这些处决是不允许发生在S. 这导致了下面的定理[3]。定理2.12设I是X上的不变量，S是某个I-约化的Y -带Y的命令X. 设S 0 从S得到如下结果：每个限制性选择S1发生在S中的S2将被替换为S12wlp（S1）（false）！S2：然后每个基本命令将被替换为它们的关于I的GCS。设Z是状态空间Y的不相交副本。用公式P（S;I;x0）fz=yg：wlp（S0 0;z=x0！skip）（wlp（S）（z=y））;其中S00通过将Y重命名为Z而从S0产生，GCSSI在语义上我我等于@0P（S;I;x0）！ S0;y=x0！ 南峡。2XI根据定理2.12对GCS的特征化使得有可能将一致性强制简化为简单的语法替换（S 0的形成）和保护的调查，即P（S;I;x0）。由于特殊化前序的定义，一般来说，GCS是高度不确定的，即使原来的程序规范不是。然而，从实用主义的观点来看，只要有一个确定性的结果就足够了。因此，考虑确定性GCS分支或至少准确定性GCS分支是一个自然的想法。在这里，准决定论意味着决定论的价值选择[7].现在让我们看一个如何在定理2.12的基础上构造GCS分支的例子。例2.13考虑状态空间X=fx1;x2 g。尽管到目前为止，p是隐式的，但让我们假设两个状态变量的值都1110我一对一对。 我们考虑以下三个X约束：I1 1（x1）1（x2）I28x; y：x2x2^y2x2^2（x）=2（y））1（x）=1（y）和I32（x1）\2（x2）=;将函数i投影到第i个分量上。然后我们考虑fx1 g上的一个程序规范S，它由简单赋值x1：=x1[ f（a; b）g，其中a和b是常数.步骤1.首先考虑约束条件I1。因为S只是一个赋值，所以它是I1-约化的。然后，我们将S替换为其GCS关于I1的准确定性分支，并获得x1 ： =x1[f （ a;b ） g; （ a2=1 （ x2 ）！ @cx2 ： =x2[f （ a;c ）gskip）这是一个X操作。让它成为我们的新S1。步骤2.现在考虑约束I2。可以证明S1是I2-约化的.我们必须删除限制性选择，然后用确定性GCSbran chc2=2 （x2 ）替 换 x 2 的 赋 值！x2：=x2[f（a;c）g，分别到我2。 对于结果操作S 我们计算P（S1; I2），为真。后通过一些重排，我们得到S关于I1^I2的如下GCS分支：x1：=x1[f（a;b）g;（（a2=1（x2）！ @cc2=2（x2）！ x2：=x2[f（a;c）g）2a21（x 2）！跳过）让这成为我们的新规格S2.步骤3.现在考虑约束I3。同样，我们可以证明I3-约化性，但与形式证明无关。我们用确定性GCS分支x1：=x1[f（a; b）g ;x2：=x2fx2x2j2（x）= bg来代替S2中类似地，我们用确定性GCS分支x2：=x2[ f（a; c）g ;x1：=x1]替换S2中对x2的赋值 fx2 x1 j2（x）= cg.然后我们计算P（S2;I3），b2=2（x2）^（a2=1（x2））8c：（c622（x2））c2=2（x1）[fbg））：经过一些重新安排，最终结果是b2=2（x2）！ x1：=x1[f（a;b）g;（（a621（x2）！@cc2=2（x2）^c2=2（x1）！ x2：=x2[f（a;c）g）2a21（x2）！skip）;11它是S的GCS关于I1^I2^I3的分支。22.3可计算性和可判定性GCS方法已经成功地开发了相对于Lar。使用算术逻辑的初衷是研究可计算性和可判定性问题。取定理2.12中GCS的一般形式，我们可能会问，我们是否能找到一个算法来计算GCS。我们可以进一步问，结果是否有效。我们将确定可以计算有效GCS的子情况[3]。命题2.14如果递归保护命令被限制在有界循环中，则GCS是可计算的，即，函数（S; I）7！SI是可计算的。然而，一般来说，GCS无法计算。2即使GCSSI可以由给定的命令S和约束I计算，其结果仍然包含前提条件P（S;I;x0）。 如果这样一个前提条件是不可判定的，那么GCS将是无效的。下一个结果主要是由于以下事实。可判定算术谓词在否定和合取下是封闭的。如果在一个受保护的命令S中循环的每一次出现都是有界的，那么我们总是可以把S写成@x1： @xn T的形式。此外，由上界定理得出@yT关于I的GCS总是ys@yTI.定理2.15设S是一个程序规范，使得每个循环都有界，且所有前提条件都可判定. 让我成为一个可判定的静态常数。 然后，我们可以计算形式为SI=@y1：@ynTI的GCS SI，其中TI具有定理2.12的形式，其中所有条件P（T0;I;x0）都是可判定的。22.4专业化秩序让我们从更实际的角度来看待一致性强制，并询问GCS是否真的与我们的直觉一致。一般来说，GCS是非确定性的，这反映了各种一致性实施策略。[7]中的方法选择GCS的一个分支，该分支与要选择的值的交互式支持例如，在一个示例中，取一个包含约束x2 p） x2 q和一个插入p，则GCS分支到自由选择q的任何新值，只要它是p[ fxg]的超集直觉上，我们更喜欢这个值是q[ fxg]，即，以保持变更传播尽可能简单然而，对于GCS分支，没有这样的“偏好”或其他说法：对于Y X上的数据库操作，GCS方法在X Y上过于宽松。另一方面，只涉及集值状态变量的多值依赖关系会导致先决条件，尽管我们可能会期望更多的变化。换句话说：对于Y X上的数据库操作，12GCS方法对Y的限制太大。这表明专门化顺序对于实施目的来说可能仍然太粗糙。3最大一致性效应保持器在引言中，我们已经解释了GCS不是形式化一致性强制的唯一可能选择。如果一个程序规范S在Y中约束状态变量，并且约束是用Y X在X上定义的，那么专业化可能对Y限制太多而对X Y自由太多。我们开发的概念，最大一致性效应（MCES），旨在克服这两个弱点的GCS方法。3.1一个激励的例子密钥概念是第2节中引入的一个密钥约束概念。 这是给定程序规范S满足的转换约束J。因此，S的约束表示S的某种效应. 因此，“效应的保留”可以通过约束的保留来形式化。 让我们先看一个例子。例3.1让我们再次回顾例2.13中构建GCS分支的执行策略。 对于包含约束I 1，GCS分支以这样的方式选择，即插入x 1之后插入x 2，如果必要的话。或者，我们可以将x1替换为：=x1[f（a;b）gbya2=1（x2）！x1：=x1[f（a;b）g s kip. 这意味着通过添加一个先决条件来限制插入，如果违反了这个条件，则什么也不做。采用全球控制系统办法不可能采取这种战略类似地，对于赋值x 2：= x 2[f（a; c）g]和例2.13中状态空间fx 2 g上的约束I 2，我们可以用x2：=f（x;y）2x2j y6=cg [f（a;c）g]代替。把这些想法放在一起，我们就可以首先用S1替换S，即a2=1（x2）！x1：=x1[f（a;b）gskip为了加强与I1的一致性。那么就没有什么可以强制执行I2了。最后，我们替换b2=2（x2）！x1：=x1[f（a;b）gskip对于赋值x1：= x1[ f（a; b）g]，以强制约束I3。因此最终结果将是a2=1（x2）^b2=2（x2）！x1：=x1[f（a;b）gskip ;13这似乎是对实施例中获得的结果的合理替代。2.13.23.2更换专业化认证订单我们现在开始正式保护这些影响。本节的目标是获得专门化阶v的特征。为了利用谓词转换器，我们将转换约束J作为程序规范本身。定义3.2每个转换约束J产生一个程序规范S（J），它可以写为：S（J）=（@x0;：; x0J！ x 1：= x0 k：k x：= x0）2循环1n1nn使用保护命令。2注意，S（J）包括状态对（;1），即，包括不终止死刑。特化序可以用来表示程序规范S关于转换约束是一致的。定义3.3程序规范S关于迁移约束J是相容的当且仅当Sv S（J）成立。2我们可以把这个定义解释为S是一个扩展的程序规范，它保持了J的效果。为了提供一个对应的bet之间的约束和transition一致speci阳离子（引理3.5），我们需要从GCS理论的以下结果。它给出了特化序的一个标准形式。一个证明见[7，应用程序。B]。命题3.4LetS和T分别在X=fx1; ： ：;xng和Y上进行了代数运算，其中XY和X的一个不相交的复本Z=fz1; ：;zn g。则wlp（S）（'））wlp（T）（'）对X上的所有状态公式'成立当且仅当fz=xg：wlp（T0）（wlp（S）（x=z））是有效的，其中T 0 通过将所有xi重命名为zi，从T得到结果。2引理3.5程序规范S关于X上的转移常数J是相容的当且仅当J是S的转移常数。证据特殊化条件S v S（J）只意味着wlp（S（J））（'））wlp（S）（'） （1）对于所有的X-公式'和wp（S（J））（真））wp（S）（真）。当我们有wp（S（J））（“）时，f对任意的X成立，对任意的M，第二个 条件总是满足的。现在将命题3.4应用于方程（1），得到：fz=xg：wlp（S0）（wlp（S（J））（x=z））：14XXxX这建议根据定义进一步简化wlp（S（J））（x=z），3.2. 这产生wlp（S（J））（x=z），：（8x0：J（x;0））06=z），9x0：J（x;0）^x0=z， J（x;z）：我们一起得到了SvS（J）ifz=xg：wlp（S0）（J（x;z））这证明了引理2推论3.6设J是一个转移约束，S是X上的一个程序规范. 则以下是等价的：(i) S与J一致，(ii) J是S的一个常数r，(iii) 对于11个X-式，2最后，我们准备通过保留特殊化约束来刻画特殊化序。命题3.7设S和T分别是Y和X上的程序规范，其中Y X。然后我们有Tv S当且仅当S的每个有fr（J）Y[ Y0的约束J也是T的一个有fr的约束，并且wp（S）（true））wp（T）（true）成立。证据考虑only-if方向rst。条件wp（S）（true））wp（T）（true）已经是我们假设成立的特化条件T v S的一部分。 设J是S的任意约束，fr（J）Y[Y0. 根据引理3.5，我们有SvS（J）。由于TvS在假设下成立，我们利用v的传递性得出T v S（J）也成立的结论。同样，引理3.5暗示J必须是T的一个约束。对于相反方向，我们只需要证明wlp（S ） （“）wlp（ T）（”）对每个ch“都成立，其中fr（”）Y。我们假设，fy0=yg：wlp（S0）（J））fx0=x g：wlp（T0）（J）对于所有的J都是有 效的，其中fr（J）Y[Y0。现在，让我们考虑一下 其中fr（'0）Y0. 那么我们可以得出结论fy0=yg：wlp（S0）（'0））f0=xg：wlp（T0）（'0）：替换可以被省略，因为它们仅是具有fr（'0）Y 0的重命名。最后，我们将y的值重新命名为y的屈服值15wlp（S）（'））w lp（T）（'）16X对于所有的'，其中fr（'）Y如所要求的。2命题3.7告诉我们，一个给定的Speci cation S的特化保持了S的所有约束条件所给出的结果，并且如果S为0，则终止。 我们论证了专业化的顺序过于粗糙。上述特征允许以自然的方式削弱这种秩序。3.3MCE的定义定制操作方法的基本思想现在不是考虑所有的业务约束，而是仅考虑其中的一些。 因此，我们不是建立S关于I的GCS，而是建立某些S（J）的GCS。如果在J中省略了S的某些约束条件，则S（J）将只执行在S的任何特殊化中不发生的操作. 这样，我们就可以避开2.4节中提到的问题。然而，采取任何这样的约束都是非常困难的。 S（J）应该只添加与I一致的执行。 这只是为了定义与X上的给定静态约束I兼容的新的约束。因此，我们只对S（J）的终止执行感兴趣，即，形式的规格S0（J）=@0J！ x：=x0：那么，与I兼容意味着构建GCSS0（J）I 我不想增加部分。 因此，如果S0（J）不是偏的，那么S0（J）I也不是偏的.定义3.8转换约束J与静态约束I兼容（简称：I 兼容）当且仅当wp（I！ S0（J）I）（false））wp（S0（J））（false）成立。2例3.9很容易看出，例2.10中的每一个约束条件都与选择为多值依赖项的I兼容。此外，这些约束中的三个约束的合取也与I相容，但所有四个约束的合取不与I相容。2定义3.8允许显示以下技术引理。基本上，它利用了GCS的交换性结果（命题2.7）。请参见附录A以获取证明。引理3.10设J是I1^I2相容的转移约束那么J是I1和I2相容的。2最后一个例子建议我们考虑下式约束的蕴涵序。我们说J1强于J2当且仅当J1）J2成立.不幸的是，S没有最小的约束条件，但我们可以按这个顺序考虑极小元。定义3.11S的一个相容约束J相对于一个静态约束I（简称：I-low）i是低的，它是I相容的，并且对于S没有严格更强的I相容的相容约束 217我有关反映保留效应的想法可以通过低成本约束最大化的结果，请参见附录B。现在我们准备为一个程序集S定义一个最大相容集。 对于这些，我们选择一个低约束J，这使S的一个效应形式化以被保留。 然后，我们采取一致的数据库操作SI;J 它保留了这个方面，但仍在ned之下，其中verS在ned之下。最后，我们需要SI;J 最大限度地发挥这些特性的作用。定义3.12设S是程序规范，I是X上的静态约束. 设J是S的一个I相容的约束。X上的一个程序规范SI;J称为S关于I和J的一致性预存器（CE）当且仅当(i) J是S1的约束条件;J，(ii) wp（S）（fals e）） wp（SI;J）（fals e）成立，(iii) SI;J 与I有关，(iv) 具有这些特性的任何其它程序实例T专门化SI;J.若J对S关于I 是even低约束的，则 SI;J称为最大一致性检验器（MCE）。2注意，在这个定义中，S所定义的状态空间不再重要。它在被选择的J里面消失了。然后很容易看出，MCE捕获了用于基本数据库操作的非正式执行策略3.4MCE的一个范式（最大）一致性检验的最后一个性质（定义3.12）再次使用了特化阶v。这似乎是令人惊讶的第一时刻，但它原来是一个自然的定义，如以下命题所示，它给出了一个标准形式的最大一致性效应。定理3.13设S是程序规范，I是X上的静态约束.设J是S的一个I-low约束。然后wp（S）（true）！S（J）是MCESI;J 与I和J有关。是的。 我们谈谈wp（S）（true）！S（J）I 作为SI;J的定义 并验证定义3.12中的每一个条件。首先，我们证明了J是SI的一个约束; 这直接从S（J）IvS（J）（定义GCS）和SI;J vS（J）I. 第二18我条件由以下计算得出：wp（S）（false），：wp（S）（true），wp（S）（true））false，wp（S）（true））wp（S（J））（f alse））wp（S）（true））wp（S（J）I）（false），wp（SI;J）（false）：SI;J的I-相合性由S（J）I关于I的相容性直接得出，即I）wlp（S（J）I）（I）蕴涵I）（wlp（S）（true））wlp（S（J）I）（I）），其中h等于I）wlp（SI;J）（I）. 最后，设T是一个程序规范，使得J是一个 T的约束，wp（S）（f alse））wp（T）（f alse）和T与I是一致的。根据引理3.5，我们得到T v S（J），因为J是T的一个双约束。与T的I-相容性一起，得出了最大相容性的定义，即evenTvS（J）I 保持。然后，我们还应用wp（T）（真））wp（S）（真）来获得T= wp（T）（true）！ T v wp（S）（true）！S（J）：这确立了TvSI;J的价值 并完成PR O。2注3.14S（J）允许在所有起始状态下不终止这些分支在SI中可以忽略;J 通过增加一个前提条件wp（S）（false）.2由于不需要利用J的低性，证明甚至给出了一致性的标准形式。推论3.15设S是程序规范，I是X上的静态约束.设J是S的一个I相容的约束.然后wp（S）（true）！S（J）I 是CESI;J 与I和J有关。2从定理3.13我们可以得出第一个结论：F或相对于I（M）CESI;J的选择（低）约束 alw_ys存在并且由S;I和J唯一地确定（直到语义等价）。（M）CE与GCS密切相关。（M）CE是除了前提条件wp（S）（true）之外稍微扩展的程序规范的GCS，即，可能的修改已纳入S（J）。19该命题表明，也有一个严格的理论（M）CE导致交换性和组合性的结果。然而，这一理论并没有2011I211I2但是我们可以检查示例3.1中的构造确实导致了MCE。4交换性结果一个强有力的理论应该具有类似于GCS一致性强制的交换性（命题2.7）的结果。 对于一个给定的复杂静态约束I1 ^ ^In，我们希望将强制执行过程分解为单个合取项Ii。刚才提到的结果甚至更进一步，允许独立于给定的顺序构建最大的一致专门化。如果我们在MCE框架内重新表述命题2.7，我们可以推测I1^I2的语义等价性！（SI1;J1）I2;J2 我1^我2！SI1^I2;J12. 这里，J1是关于I1的对于S的低约束，J2是对于S11的低约束;J1 并且J12对于S相对于I1^I2是低能量约束的。在（SI1;J1）I2;J2内，具有SI1;J1 wp（S）（t rue）！S（J1）I这当然是由I1组成的。 然而，然后我们对SI1，J1，即 wp（S）（t rue）！S（J1）IvS（J2），并加强I2-一致性. 一般来说，在这一步中，我们将放松关于I1的一致性. 因此，结果（SI1;J1）I2;J2 不一定是I1-consistent nt。 因此，MCE理论的交换性陈述失败了。命题4.1在基因组中，I1^I2！（SI1;J1）I2;J2 我1^我2！ S11、I2、J12在语义上不等价.2为 了 保 持 理 论 上 的 强 度 ， 我 们 着 眼 于 不 同 的 方 式 来 构 建MCESI1^I2;J12 逐渐地 我们可以提供以下信息。定理4.2设S是Y上的程序规范，I1，I2是X上的静态不变量，且YX. L设J为S的低成本，与I1 ^I2有关。然后我1^我2！ （SI1;J）和I1^I2！ SI1^I2;J在语义上是等价的。是的。首先，引理3.10告诉我们J是S的一个关于I1和关于I2 的 双 约 束。consistente ectpreser verI1^I2 ！SI1;J 等 于 I1^I2^wp （ S ）（true）！ S（J）I. 在SI1上强制I2一致性;J 结果为I1^I2^wp（S）（t rue）！ （S（J）I）。最后，我们应用命题2.7，得到I 1^I 2^wp（S）（true）！S（J）也就是I1^I2！ SI1^I2;J.2I1^I2