174理论计算机科学电子笔记42（2001）网址：http://www.elsevier.nl/locate/entcs/volume42.html23页一致性实施理论中的可计算性和可判定性问题Sebastian Link1和Klaus-Dieter Schewe2梅西大学信息系统系，11222 PalmerstonNorth，新西兰摘要一致性强制提供了一种替代形式化程序规范语言中的通用程序验证的方法。现有的方法在程序规格说明的语义等价类上使用偏序，称为专门化，目的是用最大一致专门化SI代替给定的规格说明S，SI与给定的静态规格说明I是一致的.底层逻辑是算术逻辑，其允许研究与SI的构造性生成有关的可计算性和可判定性问题。本文从算术逻辑的角度证明了Dijkstra演算的公理化方法，并在此基础上发展了一个新的理论，使复杂规范的最大一致特化的构造问题可以归结为所涉及的基本命令和前提条件此外，我们现在甚至能够证明，这种结构是可计算的，在温和的限制下，递归程序规范和发生的前提条件是可判定的共同类的不变量。1介绍在几乎所有的形式规范语言中，至少提供静态不变量已经成为相当标准的一方面，这允许以一种可持续的方式描述系统的语义，但另一方面，是保证一致性的任务。对于一个程序规范S和一个不变量I，这意味着S的每一次执行都从一个满足I的状态开始，也应该总是导致一个满足I的状态。 但是我们可以1电子邮件：S. massey.ac.nz2电子邮件：K.D. massey.ac.nz2001年由ElsevierScien ceB出版。 诉 操作访问和C CB Y-NC-N D链接。林克和舒威175I Iω∞限制我们自己终止S的执行，因此可以分别处理终止性和一致性问题对于一般的治疗，我们认为公理化的方法，程序语义使用谓词转换器，导致最弱（自由）preconditions。众所周知，在这种情况下，我们可以通过证明义务wlp（S）（）来表达一致性，但核实义务通常会失控。寻找替代方案使我们想到了一致性实施的想法特别是，在数据库领域，不变量的复杂性-在这种情况下通常称为完整性约束[9]-远远高于程序本身的复杂性，触发器方法已经变得非常流行，但可以证明，触发器不能解决一般问题[7]。一个不同的方法，这确实表明自己，处理最大的持续专业化（GCS）[6，8]。 考虑一个给定的程序规范S和一个给定的静态不变量I，我们试图用一个稍微修改过的程序规范SI来代替S，这个程序规范SI可以证明与I是一致的。因此，原始S的所有这可以通过在语义程序规范的等价类现有的GCS理论[6]是基于无穷逻辑Lω。为了将GCS方法从某种纯理论的一个适用的理论框架，我们必须调查GCSs的可计算性和必须建立的先决条件的可判定性为了这些目的，最好与经典递归理论[1]建立紧密的联系这将在本文中完成在第二节的开头，我们介绍算术逻辑的符号。然后我们要定义关于这个逻辑的谓词转换器应该是什么，特别是我们希望这个公理化方法与关系语义等价。因此，我们必须保证谓词变换的一些稍微修改的特征性质，即泛合取性和配对条件。到目前为止，保护命令的标准语义仍然存在，我们甚至能够在第3节中表明，递归理论可以扩展到算术情况，至少，如果我们限于某些WHILE循环。有了这个背景，我们可以在算术逻辑的基础上发展GCS方法这将在第4节中完成。许多证明遵循[6]中经典对应物可计算性通常无法实现，因为最小定点的构建需要测试语义等价性，这是不可判定的。然而，如果仅限于FOR循环，GCS就变得可计算了。这将在第5节中显示此外，我们表明，自然发生在GCSs的先决条件是不可判定的一般，但我们也表明条件，保证可判定性。我们认为，至少对于一个应用领域，即数据库已经林克和舒威176∗∗⊆→∈上述限制是可以容忍的。对于一般情况，必须应用其他一些实用的解决方案[5]。最后，我们做了一个简短的总结和展望。欲知详情，请读者参阅论文[3]。2基于算术逻辑的程序设计语义我们的研究是基于一阶算术逻辑[1，第7章]，即我们的逻辑语言只包含元数为0，1，2的函数符号0，s，+和，2. 其非正式含义通常是：常数0、后继函数、加法和乘法。为了方便起见，+和被写成fix运算符。唯一的谓词符号是相等符号=。在我们的语言中变量将是x1，x2，x3，. .我们用符号T表示项的集合，用符号F表示公式的集合在此外，让V表示变量的集合我们允许所有标准缩写，包括公式true和false。从语义上讲，我们固定了一个具有域N的结构，域N是非负整数的集合。然后0、s、+、和=以通常的方式解释。对于一个解释，考虑函数σ：V→N就足够了。根据重合定理，甚至可以给出自由变量xi在一个项或公式中。特别地，我们可以总是写σ作为一个k元组，如果自由变量的数量是k。最后，k元关系R<$Nk称为算术i，它可以用算术逻辑中的公式Q∈F表示（具有自由变量x1，.，xk），即（a1，...， ak）∈ R holds i |= σQ适用于定义为σ（xi）= ai（i = 1，.，k）。2.1公理化方法及其正当化根据[6]中关于一致性强制的现有理论，每个有限子集XV被称为状态空间。每 个 函数σ：XN称为X上的一个状态。等价地，一个状态总是可以用一个k元组表示.对于一个固定的X，让<$（=<$（X））表示X上所有状态的集合。在X中具有自由变量fr（fr）的公式F称为X-公式或X上的不变量。为了强调这些变量，我们有时会写（x），其中包含状态变量的向量x那么任何一对具有2k和k个自由变量的公式（S），R_0（S））可以被认为是定义了程序规范S的关系语义。为了方便起见，假设在S中的前k个自由变量与S的自由变量一致。根据我们的记法，我们有时会写<$0（S）（x，y）和<$0（S）（x）。因此，可以用状态对来解释，而可以用y个状态来解释。 Weinpret（σ，τ），|=（σ，τ）（S）是S的一个执行，具有起始状态σ和最终状态τ. 类似地，满足Σ0（S）的状态σ是林克和舒威177⇔ ¬¬被认为是S的开始状态，其中S的非终止执行存在.注意，关系语义的模型包括守护进程的非确定性、非终止性和部分不确定性。为了得到基于所引入的算术逻辑的公理语义，我们将S与两个谓词转换器wlp（S）和wp（S）相关联，即，从公式的（等价类）到公式的（等价类）的函数-具有标准的非正式含义：• wlp（S）（τ）表征这些初始状态σ，使得从σ开始的S的每个终止执行导致满足τ的状态τ。• wp（S）（n）表征那些初始状态σ，使得S从σ开始终止并导致满足τ的状态τ。符号wlp（S）（）和wp（S）（）对应于S关于后置条件的通常最弱（自由）前提。为了节省空间，我们经常使用符号w（l）p（S）（S）来同时引用两个谓词变换。如果这发生在一个等价物中，那么省略括号中的每一个-事物就得到了wp-部分，而仅仅省略括号就得到了wlp-部分。从我们引入的（S）和0（S），下面的定义变得简单明了。定义2.1与状态空间X上的程序规范S相关联的谓词变换器定义为：wlp（S）（x））优惠（S）（x，y）wp（S）（x））惠（y. （S）（x，y）对于任意的X-公式✷下一步是证明满足一些好条件的谓词变换器对于程序规范S的定义是足够的。条件是配对条件和稍微修改的泛合取性。这给出了关系和谓词Transformer语义之间的等价性，即所谓的反演定理。我们使用标准符号w（l）p（S）<$（S）w（l）p（S）（n），并参考到wlp（S）和wp（S）作为双谓词变换器。命题2.2谓词变换w（l）p（S）满足以下条件：wp（S）（真）惠wlp（S）（假）惠wp（S）（真）及wlp（S）（x，y））惠wlp（S）（x，y）.相反，满足这两个条件的任何一对谓词变换定义了（S）（x，y）惠wlp（S）（x=y）和0（x）惠wp（S）（false）。林克和舒威178∀⇒优惠活动优惠活动∩∅⇔证据（略）这是直截了当地表明，这两个条件成立，即，对于另外的谓词变换器f（l）p，仍然需要示出w（l）p（S）= f（l）p（S）。其主要思想是利用任意X-公式<$（x）与y的等价性. （x=y<$（y）），并应用所提供的flp对于wp-情形，我们利用配对条件以及已经证明的第一个方程✷下一个结果给出了谓词变换器wlp（S）的一个范式表示，这在许多证明中是有用的引理2.3总是可以将wlp（S）（k）写成以下形式：wlp（S）（x））惠z.wlp（S）惠（x = z）惠z（z） .证据 显然，我们有<$（x）z. X = z（z）z. （z）x=z。然后引理紧接着应用泛合取性性质。✷2.2守卫命令我们现在介绍熟悉的保护命令语言[4]，我们使用标准的基本命令和标准的构造函数。为了定义语义，我们只需要定义谓词变换，因为反演定理现在是可用的。这些定义如下：w（l）p（skip）（跳）优惠券w（l）p（fail）（失败）w（l）p（xi1：= ti1. xik：= tik）（ xik/tik}.w（l）p（S1;S2）（n）惠w（l）p（S1）（w（l）p（S2）（n））w（l）p（S1<$S2）（）惠w（l）p（S1）（）惠w（l）p（S2）（）w（l）p（S1<$S2）（n）惠w（l）p（S1）（n）惠（wp（S1）（t rue）<$w（l）p（S2）（n））w（l）p（@xj·S）（n）惠xj. w（l）p（S）（S）w（l）p（P →S）（n）惠Pw（l）p（S）（n）这里{xi1/ti1，...，xik/tik}表示变量xij被项tij同时替换。这些谓词变换的配对条件和泛合取性易于验证我们说S是一个X-命令，对于某个状态空间Xi<$w（l）p（S）（l），对每个Y-公式成立，其中XY=，且X是具有此性质的极小值。3递归保护命令在最后一节中，我们介绍了保护命令语言以及通过arith中的谓词转换器表达的公理语义。林克和舒威179≤联系我们⇔拟态逻辑到目前为止，这种语言涵盖了无限选择扩展的直线非确定性我们想更进一步，研究表示为关于适当阶的最小零点μT.f（T）的递归程序这个顺序将是标准的纳尔逊顺序[4]。不幸的是，我们不能把[4]中的非常一般的递归理论。我们必须将自己限制在简单的WHILE循环中，即，f（T）=P →S;TP →skip，其中变量T不在S. 为了方便起见，我们引入命令变量T1，T2，. .3.1纳尔逊秩序纳尔逊序的思想是，只要S1≤S2成立，则S1的每个终止执行都保留在S2中，但是S2中的终止执行可以这导致了以下定义。定义3.1纳尔逊阶的定义为：S1≤S2惠（wlp（S2）（）wlp（S1）（））（wp（S1）（）wp（S2）（））对于所有的人来说。✷我们特别感兴趣的 是fi （loop ） i∈N关 于. 因 此 ， 我们采取了一个Göodelnumbingg的保护命令，其中，为我们的逻辑提供了一个关于项和模的哥德尔数（[1，p.327f.]）。有了这个Güodelnumberinggwem，就可以用两个算术谓词Q1和Q2来表示muaew（l）p（fi（loop））（n）的所有内容。引理3.2存在k+ 2元算术谓词Q1和Q2，使得Q1（i，j，x）惠wlp（fi（loop））（f（x））.................. 当h（n（x））= j和x = xi1，.，xik.证据 对于任意的程序规范S和算术预测，可以直接定义归纳公式QJ1，使得QJ1（i，j，x）wlp（S）（n（x）），其中g（S）= i和h（n）= j成立。特别地，使用我们的Güodelnumberinggwe得到一个本原ve递归函数g′such的QJ1（g<$k（g（loop）），j，x）惠wlp（fk（loop））（f（x））满意了。则we定义谓词Q1（k，j，x）惠QJ1（g<$k（g（loop）），j，x）和Q<$（h（n），h（n），x）惠（P<$wlp（T）（n）<$$>P<$wl）的扩张，F，F∈F. 我们的结论Q1（k，j，x）惠QJ1（g<$k（g（loop）），j，x）惠Q<$（h（k），h（k），x），林克和舒威180−∧{|∈}其中h（k）= j且k（x）= wlp（f k−1（loop））（k（x））= Q1（k1，j，x）。总之，我们收到Q1（0，j，x）惠为真，Q1（k+1，j，x）惠Q<$（h（Q1（k，j，x）），j，x）.因为Q是算术的，所以Q1是递归的，因为递归谓词在primitve递归下是封闭对于Q2的陈述是完全类似的.✷本文借助于谓词定义了一个极限算子S=limi∈Nfi（loop）Q1和Q2：wlp（S）（n（x））惠益i. Q1（i，h（n（x）），x）和wp（S）（n（x））惠qi.Q2（i，h（n（x）），x）.引理3.3极限S=limi∈Nfi（loop）是l l-定义的。证据根据定义，很明显，wlp（S）（f（x））惠i.i∈N <$wlp（fi（loop））（f（x））（1）保持。由此我们通过直接计算得到了泛合取性。此外，limes定义的wp部分给出了wp（S）（f（x））惠i.i∈N <$wp（f i（loop））（f（x））.（二）在wp（S）（n）成立的假设下，我们使用等价性（2），fi（loop）的配对条件和f i（loop）i N确实是关于纳尔逊阶的链的事实，对于相反的方向，可以使用一些fi0（循环）的配对条件以及两个等价式（1）和（2）。✷3.2最小不动点现在，我们将展示如何获得WHILE循环的语义很容易看出，函数f的保护命令是单调的纳尔逊秩序[4]。则最后一个引理的直接结果是存在一个最小上界，它正好由极限算子给出要看到这一点，只需应用方程（1）和（2）以及最小上界的概念。引理3.4链{fi（loop）|i∈N}有最小上界，即li mi∈Nfi（loo p）.✷在下文中，我们使用符号μTj.f（Tj）来表示以下的最小定点：如果它存在的话。命题3.5Letf（Tj）=P→S;TjP →s kip。 则f有一个最小不动点，其值为≤，即μTj.f（Tj）=limi∈Nfi（loop）。林克和舒威181{|∈ }±⇒我证据根据引理3.4，fi（loop）iN具有最小上界S = lim fi（loop）。我们就可以利用宇宙真理-i∈N结合性性质，应用方程（2）和S≤f（S）成立的事实，导出了w（l）p（f（S））（f）惠w（l）p（S）（f）是有效的。因此，S确实是一个定点，每一个进一步的定点T都是{f i（loop）}的上界。|i ∈ N}，这使得S≤ T。✷4最佳一致专业化认证现在，在一阶算术逻辑之上发展一致性强制理论的基础已经奠定。这将成为研究可计算性和可判定性的基础。4.1一致性和专业化首先，我们必须定义一致性和特化预序。这可以完全类似于[6]中的经典情况来完成定义4.1设I是状态空间X上的不变量。设S和T分别是状态空间Z和Y上的命令，其中Z<$Y<$X。• S关于IiIwlp（S）（I）成立是一致的• T专门化S（符号：TS）i w（l）p（S）（）w（l）p（T）（T）对所有Z-公式成立.✷由于配对条件，在专门化定义中只考虑wp-部分为真就足够了wlp部分也可以以已知的方式被简化。接下来，我们将介绍一致性实施的核心概念GCS。定义4.2设S是一个Y-命令，I是X上的不变量，其中Y <$X. S相对于I的最大一致特化（GCS）是一个X-命令SI，其中SI± S，使得SI相对于I是一致的，并且每个c h包含特化T±S满足T±SI。✷首先，我们证明了GCSs的存在性和它们的唯一性语义等价。此外，关于合取的GCS可以连续且独立于给定不变量的顺序来在这两种情况下，[8，6]中的经典证明都没有发生重大变化。尽管如此，我们将在附录A中给出证明命题4.3 S关于的GCSSI总是存在的，并且在语义等价之前是唯一的。我们可以写SI=（I →S;@zJ·z：=zJ;I →skip）（<$I →S;@zJ·z：=zJ），其中z是指I中的自由变量，而不是S中的自由变量。林克和舒威182⇔我± ⇔⇒1|IP|IP {}I此外，对于两个不变量I和 J，我们总是得到I <$ J→SIJ和I J→（SI）J在语义上是等价的。✷从GCS命题4.3的形式，我们可以导出wp（SI）（true）wp（S）（true），这允许集中于谓词Transformerwlp（S）。4.2GCS的上界对于实际应用，命题4.3中导出的GCS的形式几乎毫无价值，因为它涉及在非确定性地选择任意值之后测试不变量。然而，这种形式在证明中是有用的。一个合适的形式的GCS应该建立在S中涉及的基本命令的GCSs上。让这种幼稚的句法替换的结果记为SJ。 一般来说，SJ不是昏迷指数它甚至可能不我我是S的特化，或者它可能是一致的特化，但不是最伟大的一个。后一种情况的一个例子是S=x：=x−a;x：=x+a，其中某个常数a≥0且I <$x≥0。我们现在制定一个技术条件，允许排除这一点-评估。 在这种情况下，可以证明SI±SJ保持。相应的结果称为上界定理。我我们需要命令S的确定性分支S+的概念，它要求S+S和wp（S）（true）wp（S+）（t rue）以及wlp（S+）（t rue）wp（S+）（true）对所有n成立。此外，我们需要X-命令S的δ-约束的概念.这是X上的不变量J，具有X的不相交副本XJ，其中{xJ/x}。wlp（SJ）（J）成立，其中SJ由Sby将所有xi重命名为XJI而得到。最后，我们把状态σ的特征公式记为Pσ.定义4.4设S = S1;S2是一个Y-命令，使得Si是一个Yi-命令，Yi≠Y（i = 1，2）.设我是X不变量，Y∈X. 设X-Y1={y1， . ，ym}，Y1={x1， . ，xl}，并假设{XJ1， . ，xJl}是Y 1的不相交副本，也与X不相交。则S是δ-约化形式i，对于S1的每个确定性分支S+，满足以下两个条件：x=（x， .. . ， x），x0 =（xJ， . ，x，J）-保持：1升1升• 对于所有态σ，其中= σ，我们有，如果σx/xJ。（ y1.是的。 ）是一个如果S+是δ-约束的，则它也是S+;S2的δ-约束.1 1• 对于所有态σ，其中= σ，我们有，如果σx/xJ。（ y1. 是的。）是一个如果S+是δ-约束的，则它也是S+;S2的δ-约束.✷1 1我们必须将这个定义扩展到序列以外的任意命令定义4.5设S是X-命令，I是Y-不变量，其中X为Y. S被称为I-约化的i，满足以下条件：• 如果S是fal，skip，loop或赋值之一，则S总是I-约化的.• 如果S=S1;S2，则S是I-约化的，i ∈S1，S2是I-约化的，并且S是林克和舒威1832我我我我我›→我们我δ-I-约化。• 若S是P→T，@y：：#y·T，S1<$S2或S1<$S2中的一个，则S是I-约化的且S1<$S1，且S2或T分别是I-约化的.• 若S=μT.f（T），则S是I-约化的，且n（100p）是I-约化的，对于每个chn∈ N。✷有了这些技术上的知识，我们现在可以陈述和证明上面的边界定理注意，简单地用（S1）替换一些S1<$S2，（S）我在递归操作中，会破坏所需的结果。我定理4.6设I是X上的不变量，S是某个I的推论Y-带有YX的命令。 令SJ由S得到如下：• 在S内循环的每个限制选择S1→S2将由S1→wlp（S1）（假）→S2重新表示。• 然后每个基本命令将被替换为它们的关于I的GCS。则T ± SJ对每个关于I的相容特化T ± S成立。证据证明是通过S上的（冗长的）结构归纳来完成的。在预处理、选择、限制选择和无限选择的案例背后并没有隐藏什么伟大的思想，但是这些证明需要大量的技术工作因此，我们参考经典的证明[6，p.120-122]，它们只需要稍微改变对于序列，我们也可以保留经典证明[6，App.C]，只做微小的修改。最重要的思想是利用命题4.3中的GCS的标准形式，S=S1;S2来计算wlp（SI）（x=a）和wlp（（S1）;（S2））（x=a）.然后，我们区分两种情况x=aI和x= aII.我可以假设，不失一般性，S1是确定性的这样我们就能用先进的技术表征δ--简化在第一种情况下，我们假设至少在一个状态x b中违反了专门化所需的含义。由此我们得到了S1的δ-约束，并通过δ-约化得到了S的δ-约束，其形式为x=bx/XJ。 .这就产生了矛盾。第二种情况非常相似。对于递归的保护命令（仅限于WHILE循环），我们知道最小定点的存在性，我们将证明转移到附录B。4.3GCS的一般形式定理4.6具有复合性，但它还没有给出昏迷指数关于GCSs的主要定理的思想是从SJ那些不允许在S下面的定理。证明转移到附录C。我. 这导致定理4.7设I，S和SJ如定理4.6所示。 设Z为不交林克和舒威184我我我我∈我›→状态空间Y的副本。 用公式P（S，I，xJ）<${z/y}. wlp（SJ J;z=xJ→s kip）（wlp（S）<$（z=y）） ，其中SJJ由SJ通过将Y重命名为Z，GCSSI在语义上我相当于我@ xJ·P（S，I，xJ）→ SJ; y = xJ→ skip. ✷注意，如果我们把确定性分支看作是[6]中建议的实用方法，那么定理4.7中的无界选择就消失了。我们省略进一步的细节。根据定理4.7对GCS的特征化使得将一致性强制简化为简单的语法替换成为(the形成的SJ）和调查的警卫，即P（S，，xJ）。第5节的以下结果将在很大程度上取决于这一减少，并将支持理论的实际意义。5可计算性和可判定性我们现在已经达到了这样一个阶段，在这里我们可以说，GCS方法可以成功地发展算术逻辑。因此，我们可以转向本文的初衷：可计算性和可判定性问题。取定理4.7中GCS的一般形式，我们现在可以问，我们是否能找到计算GCS的算法我们可以进一步问，结果是否有效。 两个问题的答案都是否定的 一般来说，但我们将确定可以计算有效GCS的子情况。5.1GCS的可计算性首先考虑可计算性问题。用我们的Gödelnumbh表示项和公式，g表示命令，我们已经利用了它们的可逆性。从这一点我们得到以下直接结果。引理5.1F或每个nN都是可判定的，无论n是项、公式还是保护命令的哥德尔数。✷接下来我们考虑上界SJ我 发生在GCS。由于这是J仅仅是一个句法转换，我们现在可以得出结论，（S，）SI是可计算的因此，研究P（S，I，XJ）对任意XJ的可计算性是很有必要的.这些条件涉及谓词变换器wlp（S）和wlp（SJ）。我根据我们对命令的公理语义的定义，我们知道构建这些谓词转换器是通过语法替换操作简单完成的。通过再次利用我们的Gödelnumberingh，我们得出结论：林克和舒威185≥∈∈我∈我›→IPI2对于无递归的S，（S，I，xJ）›→P（S，I，xJ）-因此（S，I）<$→SI，to o-是可计算的。然而，如果S包含一个循环，那么SJ也包含一个循环。 为了确定wlp（S）和wlp（SJI我们必须使用极限运算符。 吃一惊µTj.f（Tj）这意味着为所有iN构建wlp（f i（loop））。这是唯一可能的，如果有一些nN使得wlp（fn（loop））=wlp（fm（loop））对所有m n，mN成立。这意味着我们有一个有界循环（或等价的FOR循环）。命题5.2如果递归保护命令被限制在有界循环中，则GCS是可计算的，即，函数（S，）SI是可计算的。然而，一般来说，GCS无法计算。✷5.2一个不可判定的结果即使可以从给定的命令S和不变量计算GCSSi，结果仍然包含前提条件（Si，XJ）。如果这样的前提是不可判定的，则GCS将是无效的。在下一个命题的证明中，我们利用了算术层次[1，Ch.8]。命题5.3一般来说，包含在GCS S I的一般形式中的前提P（S，I，xJ）是不可判定的。证据（草图）作为一个简单的反例，Sx1：=t1;R（x1，x2）→@y·Q（x1，x2，y）→x2：=t2“我的天，S1“我的天，S2并考虑一个可判定的I，使得S是I-约化的。然后我们使用Proposition4.3来计算GCSSI。经过复杂的计算和一些简化步骤，P（S，I，（u1，u2））优惠2002年，J.很好（（{x1/t1，x2，z2J}. （I <$R<$Q）<${x1/u1，x2/u2}. I）（<$I<${x1/t1，x2/z2J}. （<$IR{y/yJ}. Q）（{x1/u1}. （RQ）u2=t2）。这一结果是一个在100中的公式（假设R和Q是递归的）。✷很容易看出，不可判定性是由反例中使用的无界选择算子造成的这就产生了通用的量化器，谓词Transformerwlp（SJJ）和对偶谓词Transformerwlp（S/N））的。 因此我们不得不爬上两层楼在算术层次中。但是，算术层次结构中的所有类都是关闭的我我我在有界量化下。因此，如果我们将无限选择限制为有界选择，林克和舒威1860• P→{||P}选择，即，@y（y）S满足有限y=（y），则我们实现了可判定性。命题5.4如果S是一个命令，其中无界选择只以有界选择的形式出现，则对于I ∈N0，GCS S I的一般形式中所包含的前提条件P（S，I，xJ）是可判定的。✷6结论在本文中，我们考虑了[6]中提出我们可以证明，谓词变换器的基本理论可以从无穷逻辑延续到一阶算术逻辑。 我们甚至能够通过将Güodelnumb用于术语、用于mula和保护命令来实现递归程序规范。然而，所使用的递归程序规范相对于[4]中更一般的经典理论然后我们可以证明GCS的存在性和唯一性，文[8]的可交换性结果和基本的组合性结果可以推广到新逻辑中。这允许研究可计算性和可判定性问题。我们可以证明，这两个性质一般都不成立，但对于程序规范的合理子类。接下来我们至少还要讨论三个问题。首先，我们想研究Goldfarb分类[2]及其对GCS建设的影响。其次，我们想看看削弱一致性执行的方法，例如，在[5]中提出的方法，并讨论这种方法的可计算性和可判定性。第三，也是最后，我们希望解决与基本命令有关的全球控制系统的问题和削弱的方法。特别是，很高兴看到各种关系约束类的GCS（见[9]）是什么样子的。确认作者要感谢Cris Calude和Rod Downey帮助纠正了论文早期版本中的一个证明引用[1] J. Bell，M.麦克弗数学逻辑课程。1977年北荷兰[2] E. Büorger，E. Gradel，Y. Gurevi c h. 经典的决策问题。Springer1997.[3] S.链接. 一种基于算术逻辑的协调理论。M.Sc. Thesis（德文）TU Clausthal2000.林克和舒威187我T±[4] G. 尼尔森Dijkstra演算的一个推广ACM TOPLAS. 卷11（4）：517-561。一九八九年[5] K.- D. Schewe。 一致性实 施的基础 。 In H. Jaakkola， H. Kangassalo，E.Kawaguchi（eds.）. 信息建模和知识基础X：275-291。IOS Press 1999.[6] K.- D. 舍韦湾塔尔海姆走向一致性执行理论Acta Informatica.第36卷：97-141。1999年[7] K.- D. 舍韦湾塔尔海姆 在转换规范的上下文中完整性维护的规则触发系统的局限性。《控制论学报》第13卷：277-304页。1998年[8] K.- D.舍韦湾Thalheim，J. Schmidt，I.韦策尔面向对象数据库中的完整性强制。在us利佩克湾Thalheim（eds.）模拟数据库动态：174-195。计算机工作坊。Springer 1993.[9] B.塔尔海姆关系数据库中的数据库管理。Teubner 1991.AGCS的存在性、范式表示和交换在附录中，我们给出了命题4.3的详细证明命题4.3 S关于的GCSSI总是存在的，并且在语义等价之前是唯一的。我们可以写SI=（I →S;@zJ·z：=zJ;I →skip）（<$I →S;@zJ·z：=zJ），其中z是指I中的自由变量，而不是S中的自由变量。此外，对于两个不变量I和 J，我们总是得到I <$ J→SIJ和I J→（SI）J在语义上是等价的。证据首先，我们证明了GCS的存在性和唯一性，直到语义等价。我们设定T ={T|T±S和T与I一致。如果关于特化的最小上界S1存在，则这一定是GCS。因此，我们有唯一性的语义等价。现在我们验证定义4.2中的条件，以用于程序规范林克和舒威188±我的天优惠活动我来了我上面的SI设λ是Y上的任意状态公式。然后我们收到wlp（SI）（）惠（I wlp（S）（zJ. {z/zJ}。（一 ）（<$Iwlp（S）（zJ. {z/zJ}.））惠（I ）惠（I）{z/zJ}。I）（<$Iwlp（S）（））⇒（Iwlp（S）（））（<$Iwlp（S）（））惠wlp（S）（） 。这样做，我们利用了双谓词变换器然后，断言的专门化S1S从针对wp而不是wlp的相同计算得出。接下来我们考虑wlp（SI）（I）优惠（I）wlp（S）（I）优惠（I）{z/zJ}。（一））（<$i）p（S）（zJ. {z/zJ}。（一））惠（<$Iwlp（S）（zJ. {z/zJ}。（第一卷））。由于<$wlp（SI）（I）惠<$I<$wlp（S）（zJ. {z/zJ}。I）我们得到I_wlp（SI）（I），这意味着上述SI确实关于I是一致的。设x=y是一个特征态公式，T±S是任意的，但S. 然后我们再对这两个案子进行判决。案例1. 我们假设x = y因此，我们得出wlp（T）<$（x=y）WLP（T）利用wlp（S）的单调性和T.此外，wlp（T）<$（x=y）<$$>I<$wlp（S）<$（x=y）i{z/zJ}。x=y）wlp（SI）对于第一个含义，我们简单地使用特化T ± S，对于第二个含义，我们指的是应用于x=y的单调性Y。{z/zJ}。x=y，最后一个从计算wlp（SI）的第一行开始案例2. 现在我们从x = y出发，从而导出wlp（T）<$（x= y）wlp（T）<$（x = y）。利用T S和wlp（S）的单调性，我们得出：wlp（S）（zJ. {z/zJ}。（I <$x=y））<$wlp（S）<$（<$zJ. {z/zJ}。（x=y））.（1）O bviousl y，wehe（wlp（T）<$（x=y）<$I）<$（wlp（T）<$（x=y）<$< $I）和林克和舒威189I2I2我我我I2I2I1与（）一起，我们收到wlp（T）（x=y）⇔（I ）p（S）p）{z/zJ}。（I x=y）（<$Iwlp（S）（zJ. {z/zJ}。x=y））⇔wlp（SI）<$（x=y）.这第一步使我们得到wlp（T）<$（x=y）和wlp（SI）<$（x=y），即，wlp（SI）（x/=y）|wlp（T）（x/=y）。对于任意的状态公式，我们有<$（x）惠<$y。<$x（y）<$x/=y，因此wlp（SI）（x）⇔很好<$wlp（SI）（x/=y）⇒很好<$wlp（T）（x/=y）⇔wlp（T）（x）），使用WLP的泛合取性属性。由于T ± S的特殊化和wlp（SI）的首次计算，我们得到了对所有的ε，wlp（T）<$（ε）<$wlp（S I）<$（ε），并且在此基础上，wlp（T）<$（false）<$wp （S）<$（fals e）<$wp（SI ）<$（false）同样成立。事实上，我们已经证明T是SI的一种特殊化。让我们现在考虑断言的可比较结果。因为（S11）是I2-由定义weheI2组成I2=p（（SI1））（I2）.另一方面，我们可以使用GCS和一致性的定义以及（SI1）±SI1来接收I1wlp（SI1）（I1）wlp（（SI1）I2）（I1）.总之，这导致I1I2wlp（（SI1）2）（I1）wlp（（SI1）2）（I2）惠wlp（（SI1）2）（I1I2），因此我们已经提供了（S11）的一致性对于I1I2。从I2SI1±S和（SI1）±SI1是推导出来的wlp（S）（）wlp（SI1）（）wlp（（SI1））（），即、特殊化（S11）±S。因此，这与定义，反应4.2产率（S ）I2I2±SI1 I2我们将获得wlp（I1<$I2→SI1 <$I2）（I）⇔I1I2wlp（SI1I2）（）⇒I1I2wlp（（SI1））（）I2林克和舒威190⇔wlp（I1<$I2→（SI1））（S）I2林克和舒威191II→1 2 I1I2II我I2对于任意的（（S）），则仍需说明其反特殊性。I2从SI1到S I2±S，如下所示）±（I1<$I2→SI1 <$I2）。我们，（I1<$I2→SI1<$I2）±S.（A.1）此外，SI1I2 与定义的I1<$I2相一致，因此不仅有1 2wlp（SI1<$I2）（1），而且有 1 2wlp（SI1<$I2）（2）。接下来我们考虑（I1wlp（I1I2→SI1I2）（I1））惠（I1I2wlp（SI1I2）（I1））（A.2）和（I2wlp（I1I2→SI1I2）（I2））惠（I1I2wlp（SI1I2）（I2））。（A.3）从方程（A.2）我们得到I1<$I2→SI1<$I2关于I1的相容性，并利用方程（A.1）得到（I1I2→SI1I2）±SI1。（A.4）由式（A.3）得出I1<$I2→SI1<$I2与I2的一致性，由式（A.4）得出（I1<$I2→SI1 <$I2）±（SI1） 。（A.5）最后，我们计算w（l）p（I1<$I2→（SI1）I2）（）惠I1<$I2<$w（l）p（（SI1）2）（）I1I2I1w（l）p（I1I2→SI1I2）（I）惠I1I2（I1I2w（l）p（SI1I2）（））惠I1I2w（l）p（SI1I2）（）惠w（l）p（I1<$I2→SI1 <$I2）（π）特殊化I1<$I2→SI1<$I2±I1<$I2→（SI1），其中我们只使式（A.5）的应用。这就完成了证明。B递归情形下上界定理的证明在本附录中，我们证明了形式为f（S）=P →T;SP →的简单WHILE-循环的递归运算的上界定理林克和舒威192±≤→我我{|∈}跳跃，我们知道存在的最小定点根据分段3.2. 为此，我们需要一些额外的引理。对于递归保护命令，所有操作构造器关于纳尔逊阶的单调性不幸的是，类似的结果并不适用于专门化顺序。更准确地说，对于第一个组件中的构造函数，结果为false引理B.1设f（S）是一个带有程序变量S的保护命令表达式，其中不出现限制选择项。则f关于特殊化阶±是单调的。证据（略）证明是通过结构归纳法完成的。对于每个构造子，它完全类似于[4]中Nelson阶的相应证明我们省略细节。✷在[6，命题20，p.120]中，我们已经看到SJ我 可载有以下选择─构造函数，而不是限制选择，只要我们包括一些后卫。再-在递归运算中放置一些S1<$S2乘（S1）<$（S2）将破坏所需的结果。我我下一个引理来自于将上界定理中关于预条件、选择、无界选择和限制选择的 情 形 结 合 在 一 起。引理B.2设T是某个I-约化的f（S，J）关于I的一致特化，其中f（S）是由保护命令的构造函数构造的表达式.由f（S）构造fI（S）如下：(i) 在f（S）中出现的每个限制选择S1和S2将被替换为S1→wlp（S1）（false）→S2。(ii) 然后，每个基本操作，即，跳过和分配将由他们关于I的GCS代替。然后我们有T ±fI（SJ）。✷正如在经典中一样，我们现在必须面对的主要困难是把两个不同的偏序，即特殊化序±（它是GCS的基础）和递归所需的纳尔逊序≤引理B.3设T和S是Y-运算且{fi（loop）|i ∈ N}是关于Nelson序的Y -运算链。此外，设I是X上的不变量，对于Y<$X。然后我们有：(i) 如果T ≤ S成立，则TI≤ SI成立。(ii) （li mi∈Nfi（loop））±limi∈N（fi（loop））I.证据（i）这里我们使用命题4.3中给出的GCS的标准形式。第一个结果立即出现，因为所有构造函数在纳尔逊阶≤中是单调的。（ii）首先，limi∈Nfi（loop）是fi（loop）iN的最小上界关于根据引理3.4的纳尔逊阶，
我的内容管理
展开
