50网址：http://www.elsevier.nl/locate/entcs/volume70.html20页Z规格说明与证明Susan Stepney苏珊·斯特普尼1，2Logica UK Ltd，Betjeman House，104 Hills Road，Cambridge，CB2 1LQ，UK。Fiona Polack3 Ian Toyn4约克大学计算机科学系Heslington，York，YO10 5DD，UK.摘要一旦你证明了你的修正是正确的，这不是结束。 真正的产品及其附带的规格随着时间的推移而发展，新的改进版本增加了功能。在更改和升级先前存在的大型规范及其相应的证明时，会出现新的维护问题我们展示了如何使用重构的概念来构建这个过程，并提供了一种定义良好的、有纪律的修改方法。此外，我们还讨论了证明和重构之间的类比，作为保留变换的意义，可以用来建议开发重构工具集，从而改进工具集。关键词：Z，细化，重构，模式1介绍Logica[10]报告了与执行这些工业规模的Z证明有关的一些问题，并概述了证明工具支持的一些要求，以帮助完成这项任务。1电子邮件：susan. cs.york.ac.uk2现住址：约克大学计算机科学系，Heslington，York，YO10 5DD，英国。3电子邮件地址：fiona@cs.york.ac.uk4电子邮件地址：ian@cs.york.ac.uk2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。51当系统进行维护和进一步开发时，必须跟踪其配套规范和证明。在这里，我们将讨论这些大规模规范和证明的后续维护中出现然后，我们将讨论重构的概念如何用于阐明工具支持的要求，并讨论如何将证明工具视为重构工具的第一步这里给出的例子是在Z中给出的，因为它们是从Z规格导出的。然而，这些概念在很大程度上是独立于语言的2维护即使从头开始规范和证明任务，商业开发也很少从一张白纸开始通常，实现细节会限制可以做什么，以及如何构造规范。当增强现有规范时，比如升级功能，这些约束就更加重要。2.1影响分析通常，客户决定所需的升级，并要求将其添加到规范中。在简单的情况下，这可能只需要添加一个操作（假设状态和操作样式规范）来捕获新功能。在更复杂的情况下，它可能还需要添加更多的状态来捕获新函数的工作方式。甚至更复杂的情况可能需要对规范进行根本性的更改，因为更改可能会颠覆原始的建模假设维护过程的一部分是影响分析：在进行更改之前确定拟议更改的成本和后果对正式规范和证明的影响应包括在此影响分析中，以便客户能够意识到在他们看来是一个简单的实施变更的实际影响。例如，在LFM的一个项目中，当客户添加一个具有不同执行风格的操作时，我们遇到了一个问题。这个新的操作使用推模型（系统等待命令，然后响应它得到的任何命令），而所有其他操作使用拉模型（系统积极循环，直到完成处理命令序列）。模型的改变对实现的影响很小对规格的影响略大。我们不得不修改规范，以包含一个作为全局状态组件的标记，该标记在除了新操作之外的每个操作中都显式地切换，从而避免了每个操作。我们还必须提供一些微妙的论证，说明这个全局指定变量如何对应于实现与正式方法小组的早期磋商可能会导致不同的结果。52设计2.2保持惯例在维护过程中，还必须保持规范的非正式部分是最新的。索引、注释和布局约定都需要维护。如果这些约定没有被记录下来，这可能是困难的。在LFM因此，我们已经开始为这些约定描述一些简单的模式[13]，以帮助最初的规范过程，并帮助维护。3重构当升级涉及添加操作和状态组件时，规范会变得越来越复杂。对一个正在经历如此持续发展的规范进行结构改进是至关重要的，否则即使是最优雅的规范也会很快退化成不可理解的符号汤。重构[4]是一种以规范、可控和可管理的方式改进代码结构的技术。它是一种在不改变行为的情况下改进设计的技术。特别是，重构可以用来确保演化的代码使用所需的模式[6]。每一个单独的重构更改都非常小，比如重命名一个组件，或者移动一个特性，或者拆分一个方法。因此，每个变化都可以单独理解和测试。对代码结构的大的改进是通过对某个目标应用一系列这样的小的受控更改来实现的。作为XP规程的一部分，重构被特别强调[2]，XP规程在很大程度上依赖于渐进式的设计和编码方法。Cleanroom开发过程[3]允许在输入到输出函数不变的情况下更改组件，可以被视为意义保持重构的早期示例。3.1重构一个规范和证明这些重构的概念很容易应用于形式化的规范和证明开发，如下所示数学家特别喜欢重写证明，使它们更清晰、更通用或更简短。在本文中，我们讨论的是一个更具体的学科：一个特定的过程（在小的控制步骤中重构），以实现一个目标（更好的结构，以帮助维护和升级）。正式的重构本身不应该改变规范的含义（我们不去定义一个具体的含义。可能53是由诸如Z的国际标准[7]之类的东西给出的模型集它可能是一个较弱的概念，如它可能是某种较弱的意义，与特定的具体上下文有关。）然而，重构可能是升级规范和证明之前或期间的一个可取步骤（升级将改变含义）。重构可以应用于规范以改进其结构，在这种情况下，更改需要通过任何已验证的证明进行传播重构可以应用于规范，以改善后续证明的结构。重构可以单独应用于证明，以改进其结构，而不考虑具体说明。3.2小步骤正式重构的第一条规则，就像代码一样，是在小的、受控的步骤中进行更改。每个重构步骤都应该是可以进行的最小的逻辑上完整的更改，并通过规范和证明一直推进（规格的一个小变化可能会对证明产生巨大的连锁反应这是重构步骤应该尽可能小的另一个原因不要屈服于一次性进行几个大的彻底更改的诱惑：很容易迷失在更改的泥潭中，忘记或错过对证明的必要更改如果变化很小，则更容易定位小的步骤也更容易记录，并记录在更改列表中。例如，LFM的一个在最初的规范开发的早期，我们将状态划分为四个相当独立的子状态（独立是因为很少有谓词涉及不同子状态中的组件，并且大多数操作都改变单个子状态中的组件）。在随后的一个升级周期中，我们清楚地看到，其中一个状态组件及其相关的预测将更适合不同的子状态，因为它将导致引用多个子状态的谓词和操作明显减少。我们在一个重构步骤中移动了声明和谓词，通过操作定义和证明来推动所需的更改这是我们所能做的最小的逻辑上完整的步骤：采取两个步骤（声明，然后谓词，说）会留下中间规范类型不正确和不可证明。在尝试重构的过程中可能会引入错误（特别是在目前，工具支持尚未完全开发的情况下）。此外，一些重构步骤可能会导致对规范的更改比预期的要大，特别是证明。如果重构带来的好处很小，那么最好恢复而不是继续进行大的重构。因此，请确保可以回滚每个更改（使用版本54控制系统），以便可以从错误的重构尝试中恢复。3.3识别重构重构的机会随着专业人员获得经验而变得更加明显。此外，在形式化重构中，执行证明的过程以这种方式获得的经验教训可以建议重构以改进结构。在做证明时学到的经验教训可以用来建议对规范的重构。例如，在Purse项目中（见前面），我们注意到状态组件的某些组合出现在精化证明中，并且这些组合映射到应用领域中有意义的概念。因此，我们将这些作为派生状态分量引入规范这种重构改进了规范和证明的清晰度和结构在做证明时学到的经验可以用来重构证明本身。例如，在Purse项目中，我们意识到我们要多次证明类似的属性。我们参数化了这个属性，将其提取为已证明的引理，然后在主要证明中多次使用它这缩短和简化了主要的证明。引理作为应用程序域中的属性是有意义的，因此这种重构也使证明结构更容易理解。3.4更改控制清单重构可以简化更改控制列表，并使更改看起来比实际上更大，这可能会使任何期望只评估一个小升级的第三方感到在LFM的项目中4证明重构[4]描述的代码重构过程必须进行修改，以重构不可执行的规范。对于代码重构，测试是非常重要的。必须在每个小的重构步骤之后执行回归测试套件，以确保代码没有被破坏，并且含义没有被改变。由于每一步都很小，因此任何由更改引入的错误都应该可以快速检测和修复。使用规范重构，运行回归测试套件的类似操作是进行类型检查、定理证明和验证。554.1类型检查类型检查会捕捉到一些小的、愚蠢的错误。这很容易通过正式的符号支持工具来执行4.2定理证明接下来，重构通过证明传播：这涉及到首先进行更改，然后确保所有推理步骤在这些更改后仍然这有时需要对证明进行相当大的修改重构的步骤应该尽可能的小，部分是为了确保这些证明的变化不会太大。这一步用来暴露任何变化的具体化的意义，一个检查这些定理被证明。4.3验证仍然存在这样的可能性，即一个变化可能会改变具体化的意义，但不会改变其任何定理的有效性问题来了，这是一个问题吗如果具体化和证明捕获了一个精化关系，那么对意义的改变不会使精化失效，这可能不是问题。如果对除精炼以外的属性感兴趣，例如，安全或安全属性，则需要更加小心。应根据非正式要求重新确认变更例如，LFM的一个规范最初有几个在“受益”步骤中因为在抽象模型中没有任何东西需要约束我们通过（非正式的）验证来证明这种变化：这些约束不是被指定的系统的必要属性，仅仅是更具体的设计的属性4.4更多定理重构应被视为一个机会，以捕捉进一步的期望，但隐含的属性的规格。这些理想的性质可以表达为定理，需要重构后重新证明 这些定理作为“回归证明套件”，以确保进一步的重构是正确的。4.5增量重构过程虽然重构是最小的增量更改，但某些单个重构可以分解为更小的、部分可检查的步骤。即使整个规范和证明部分不一致，56通过这些步骤，可以检查其部分。例如，在细化证明的上下文中，• 修改和检查抽象规范• 修改和检查关于抽象规范的证明• 修改和检查具体规格• 修改和检查有关具体规格的证明• 修改并检查检索关系规范• 修改和检查精制校样在任何步骤中，都可能发现错误（例如，全局属性不成立）。这可能需要修改以前的步骤。5有用的重构在本节中，我们将描述Logica形式化方法团队在其各种Z项目中发现的一些有用的重构。其中一些只是为了改善和澄清结构。其他的也是为了符合各种Z约定，如[1]所示，目前在[13]中被捕获这些项目中的证明都是手工完成的，只有最少的工具支持（仅类型检查）。这些规范和证明是独立评估的;一些结构上的改进旨在使这些证明的评估更容易。不同的重构可能更适合于工具支持的证明。(See稍后还会讨论重构过程的工具支持。）许多重构都可以在任何一个方向上应用（因为它们意味着保留）。在特定情况下选择哪个方向取决于具体的背景。其目的是改进规范和证明的结构、可读性和可修改性。每个重构的语句都具有以下结构（为了简洁起见，有些部分可以省略• 名称• 对问题的简短陈述• 重构更改的简短声明• 讨论• 实现重构所需遵循的流程步骤• 例如5.1重命名组件您有一个指定组件，其名称没有指明其用途，或者违反了命名约定。 换个名字。57···这种重构在规范化的早期阶段最为有用随着规范的发展和组件用途的明确，最初的名称选择可能变得不合适。最初的名称可能过于暗示（包含更多的在这一点上，命名约定也经常发生变化。保持名称的意义和一致性使规范更具可读性。• 选择新名称• 必要时更新命名约定文档• 重命名定义• 在整个规范和证明中传播名称更改。类型检查器可用于帮助查找所有需要更改名称的位置。5.2提取共性你有一个术语在规范或证明中的几个地方使用引入一个新的定义，为术语提供一个名称，并使用该名称代替术语。确保新命名的术语本身是一个有意义的概念，而不仅仅是来自文本的巧合。让名称捕捉这个含义（并遵循任何命名约定Pattern）。名称的使用使规范更具可读性，更简洁。“新名称可以作为全局定义（可能是一个新的工具包定义）、模式、派生状态组件、局部定义（存在性量化）或引理（在这种情况下，“名称”出现在非正式注释中，而不是正式文本中）引入• 创造新的定义• 类型检查，以确保没有名称冲突• 对于定义范围内术语的每次使用，用名称类型检查，以确保名称已正确使用，在这种情况下，通过证明传播替换（这可能需要添加扩展步骤，当使用定义时，在证明中的每个点用其定义替换名称5.3内联名称你有一个定义相对简单的名字，只使用一次或几次。将其名称删除，并用其定义替换其用途。这本质上是逆向的提取公共性重构获得正确的组块大小是一门艺术。名字太少，读者必须58解开了大量的数学难题太多的名字，读者不得不记住他们的意思时，困惑他们的用途。• 每次使用这个名字· 用它的定义替换它的名字· 类型检查，以确保名称已正确使用• 删除名称的定义• 类型检查，以确保没有遗漏使用5.4将笛卡尔积更改为模式积您有一个Caribbean产品类型被用作记录，其中包含许多组件引用。 引入一个架构产品类型，并使用它。一个卡宾枪乘积的分量是由它们的位置来标记的，这是一个没有太大意义的数字。模式产品的组件由它们的名称标记，可以选择更有意义的名称• 使用新名称创建新定义（如果新旧定义的名称相同，则首先进行重构以重命名旧定义）• 类型检查，以确保没有名称冲突• 将每次出现的旧名称更改为新名称，并将每次出现的零部件引用从编号更改为名称（这将需要更多的机械更改，请参见示例）。• 类型检查，以确保名称已正确使用• 通过证明• 删除旧定义• 类型检查，以确保没有遗漏使用前面的例子：一个句法结构被定义为一个加减乘除积;它的语义通过意义函数应用于编号的成分。binOp==EXPR×OP×EXPRb：binOp·Meb = Mob。2（Meb. 1，Meb. 第三章例后：句法结构被定义为一个模式产品;它的语义通过意义函数应用于命名的组件。BinOp==[lhs，rhs：EXPR;op：OP]MeθBinOp=Moop（Melhs，Merhs）595.5拆分状态组件您有一个产品类型的状态组件，其中每个组件都独立于其他组件被引用 对于产品的每个部分，用单独的组件替换单个组件。产品类型的各个部分是独立作用的，因此不需要捆绑在一起。之前的结构S == [c：A×B;. | P (c. 1）; Q（c. 2）;. ] 的一种结构后：S == [ca：A; cb：B;. | P (ca); Q (cb);... ]5.6合并状态组件您有两个或多个状态组件，它们经常被一起引用。用一个产品类型的组件（carpet或schema产品）替换单独的组件各个独立的组成部分作为一个更大的整体的一部分发挥作用，因此可以结合成一个整体。之前的结构S == [ca：A; cb：B;. | P (ca, cb); Q (ca, cb,.. . ）;... ] 的一种结构后（carbohydrate产品）：S == [c：A×B;. | P (c); Q (c,.. . ）;... ]的一种（schema product）之后的结构：C== [ca：A;cb：B]S == [c：C;. | P (c); Q (c,.. . ）;... ]的一种如果某些同品种部件也可以捆绑，则（carbohydrate产品）之后的替代结构C=={ca：A; cb：B |P（ca，cb）}S == [c：C;. | Q (c,.. . ）;... ]的一种（schema product）之后的替代结构C == [ca：A; cb：B;. | P (ca, cb)]S == [c：C;. | Q (c,.. . ）;... ]的一种5.7将状态拆分为子状态你有大量的国家组成部分。 把国家组织成子国家。60较小的状态块可能更容易理解，并且可以简化操作定义。相互约束的组件和一起更改的组件是处于同一子状态的候选对象。大多数状态谓词都在子状态上，很少在全局状态上。此外，大多数操作只会检查单个子状态，其他子状态的不变性质可以通过一些检查模式来捕获，而不是一长串不变的状态组件。• 定义子状态模式;类型检查• 修改状态模式以使用这些;类型检查• 修改每个操作模式以使用这些模式，包括使用子状态模式和子状态模式;类型检查• 定义子状态初始化操作;类型检查• 使用模式演算来定义使用子状态初始化的状态初始化操作;类型检查• 修改初始化操作以使用这些;类型检查• 通过证明传播。这种重构之后可以缓慢地扩展模式，以利用在模式扩展步骤期间仅扩展相关子状态的机会（这可能导致添加一些额外的步骤，因为子状态被逐个扩展）。前例S==[x，y：Z; a，b：PZ|x ∈ a; y/∈ b; a/= b]Op==[X]S;x？ ：Z |x J= x？; aJ=ax？;yJ=y;bJ=b]InitS==[SJ|xJ=0;yJ=1;a J={xJ};b J=0]例如在Sx == [x：Z; a：PZ|x∈a] Sy== [y：Z; b：PZ|y/∈b] S ==[Sx; Sy|a/= b]Op==[Sx;Sy;x？ ：Z |x J= x？; aJ=ax？]的一种InitSx==[SxJ|xJ=0;a J={xJ}]InitSy ==[SyJ|yJ= 1; bJ= 0] InitS ==InitSxInitSy5.8在子状态之间移动状态组件您有一个子状态组件经常与另一个子状态中的组件一起使用将元件移动到另一个子状态。• 根据需要移动组件和任何谓词61Op==Op 1oOp 25.9将操作拆分为析取操作你有一个操作，它的谓词中有一个顶级的析取符将操作分成两部分，每个分离符一个。前例Op == [S| P; Q R; S]例如在OpQ == [S| P; Q; S]OpR == [S| P; R; S]Op==OpQ=OpR5.10将操作拆分为组合你有一个操作，其中一些存在量化的状态分量充当在这些组件上将操作拆分为两个，并组合各个部分。这有效地扩展了模式组合5的定义。前例Op==[S| <$S0· P（θ S，θ S0）<$Q（θ S0，θSJ）]后的示例Op 1 == [S| P（θ S，θ SJ）]Op2 == |Q（θ S，θ SJ）]95.11通用定义你有几个类似的定义作用于不同的类型。 定义一个通用的结构来捕捉所有的行为。这是提取公共性的一个特例。5.12Curry函数您有一个产品类型的函数参数，但希望仅将该函数应用于该产品的一部分将产品类型替换为咖喱形式。前面的例子5这表明应该对模式管道进行类似的重构。然而，由于我们还没有遇到一个大规格管道的现实情况，我们省略了描述。629加法：N×N→N增量：N→Nm，n：N·add（m，n）=m+nn=add（1，n）以下示例添加：N›→N→N增量：N→Nm，n：N·add m n=m+nincrement=add 15.13重新排序产品参数您有两个函数，一个具有产品范围，一个具有产品域，您想要组合它们，但是产品具有不同顺序的项目。重新订购其中一种产品以匹配另种产品。前面的例子f：X<$→Y×Zg：Z×Y<$→Wh：X→Wx：X·y：Y; z：Z|（y，z）= f x·h x = g（z，y）示例：f：X<$→Y×Zg：Y×Z<$→Wh：X→Wh=fog5.14重新排序咖喱参数你有一个你想部分应用的函数，但是参数顺序不支持。重新排列参数，以便它可以部分应用。前面的例子f：X<$→Y<$→Zg：X›→Zy=Y·x：X·f x y=g x以下示例63f：Y<$→X<$→Zg：X›→Zy：Y·f y=g5.15早瘦，常瘦目标被证明的假设是庞大而笨拙的。尽可能早地、尽可能经常地淡化假设从假设中精简声明和谓词有两个优点：它使假设保持较小和可管理;它更清楚地表明了剩余的属性仍然需要履行剩余的目标。5.16将公共校样步骤移到分支点之前你有一个分支成几个“情况”的证明 在案例拆分之前移动步骤，并且仅执行一次。如果每个分支中的步骤只是5.17把一个普通的证明步骤变成一个引理这是提取公共性的一个特例。确保引理是有意义的，而不仅仅是一个5.18缓慢扩展架构您有一个很大的或嵌套很深的模式，它在一个步骤中被扩展或扩展，导致突然出现许多（到目前为止）不必要的术语。增量地扩展模式，只暴露在任何给定阶段所需的那些术语。这 可 能 需 要 先 使 用 Split a state into substate 或 Split an operation intodisjuncts重构。如果模式在目标假设中用作谓词根据需要使用术语，然后细化它。646意思是改变重构改变了结构，但没有改变意义。其他步骤看起来像重构步骤，但确实改变了规范的含义，仍然可以使用，以修复bug，整理不合理之处，并以可管理的方式升级规范在应用这些“有益因素”时，使用了与重构中使用的相同的原则，即只采取小的、可证明的、受控的步骤例如，请参见删除不必要的抽象约束的情况（之前）。将重构（改变结构而不改变含义）与受益（改变含义而不改变结构）分开可以帮助为维护和升级过程提供一个有纪律的框架。下面是我们对LFM项目的一些捐助。6.1更改类型功能更改可能需要更改组件的类型。例如，简单类型可能需要扩展为产品类型。在添加任何新功能之前，对类型进行最小的更改（因此，始终添加新组件，但• 修改抽象模型中的类型;类型检查• 修改关于抽象模型的任何全局性质证明• 修改具体模型中的类型;类型检查• 修改关于具体模型的任何全局性质证明• 如果合适，修改链接已修改类型的检索关系;类型检查• 根据需要6.2添加状态组件上面的类型更改参数适用于一个稍微大一点的上下文中，将一个状态组件添加到一个SQL/SQL规范中，以便添加更多的功能。• 将组件添加到抽象模型;类型检查• 添加抽象约束;类型检查• 修改关于抽象模型的任何全局性质证明• 将构件添加到混凝土模型;类型检查• 添加具体约束;类型检查• 修改关于具体模型的任何全局性质证明• 修改检索关系以链接新的抽象和具体组件;类型检查65• 根据需要6.3添加操作在通常的类/类风格的模型中，添加一个操作对规范几乎没有影响。如果模型具有关于全局性质的定理，则有必要修改它们的证明以确保性质仍然成立。• 将操作添加到抽象模型;类型检查• 修改关于抽象模型的任何全局性质证明• 将操作添加到具体模型中;类型检查• 修改关于具体模型的任何全局性质证明• 在精化证明中添加一个新分支以覆盖新操作6.4添加函数参数类似地，为函数添加另一个参数首先添加参数，然后分别添加约束。7重构作为一种证明技术重构的概念可以在执行（手工）证明时使用。一个证明可以被认为是一个目标的一系列意义保持转换的文档，这些转换以特定的方式改进了它的结构，使谓词为真。许多证明步骤可以以向前或向后的方式应用，因此是意义保持的。例子包括单点或应用莱布尼茨（用等号替换等号），模式扩展和各种消除。这些步骤可以被视为重构。证明的呈现可以通过重复以下步骤来构建• 复制并粘贴目标的最新形式• 通过适当地编辑副本来执行所需的重构• 类型检查为了演示的简洁可以在目标的单个副本上执行几次然而，为了使这样的呈现步骤能够被评审者理解，被重构改变的目标的单个部分不应该被同一步骤中的后续重构进一步改变（即，将多个重构限制到目标的不同部分执行的重构的名称构成证明步骤文档的一部分668工具支持代码重构可以检查整个程序。例如，更改方法的名称涉及到在调用该方法的每个位置进行更改。然而，尽管这种变化很普遍，但却很肤浅。更深的代码重构往往包含在代码的小区域中。通过进行小的更改（深度小或宽度小），代码重构是可管理的。形式规范和证明重构往往有更广泛的影响，因为规范的变化对证明的影响。例如，将组件或谓词添加到状态可能涉及将其添加到每个操作的证明。同样，这些变化往往是肤浅的：添加可能对大多数操作几乎没有影响。但是，每个证明都需要检查，如果没有合适的工具支持，这可能会很繁琐目前正在构建支持代码重构的工具。例如，最新版本的JBuilder包括一个重构向导。类似的工具支持（在一个证明工具中）对于形式化重构来说是一个好处。这样的工具可以支持常见的重构模式，• 把一个州划分为若干子州• 在子状态• 将一个复杂的操作分解为多个析取操作• 将一个复杂的操作分解成一个顺序的组合• 提取一个公共子证明作为引理同样重要的是支持通过证明推动相对较小的更改。这就需要为机器生成的证据参数化策略的设施。9重构与证明的统一我们已经看到，重构是一种在规范上保持意义的转换，使其更接近结构良好的模式，而证明是一种在目标上保持意义的转换，使其更接近真实。在本节中，我们将使用这种类比来探索如何将证明和证明工具中的概念扩展到构建重构工具和重构模式语言。9.1重构策略证明工具倾向于依赖于一小部分基本推理步骤的核心集，具有所需的可靠性和覆盖属性，结合在一起使用某种策略语言产生可用的推理。这个类比表明重构工具应该依赖于一个小集合67合适的重构（有点像上面介绍的那些），然后使用某种重构组合语言，结合组合，选择，迭代和强大的模式匹配，将它们组合起来产生大规模重构（几个小的重构产生所需的模式）9.2重构整个文档一个证明工具转换一个单一的目标;一个重构转换整个规范和证明。然而，规范和证明文件可以被认为是一个单一的实体，由三个部分组成：定义（通常被称为规范），定理（我们可以假设只有一个，而不损失一般性，简单地通过将任何单独的结合起来）和策略，如何在声明的上下文中将初等推理规则应用于定理的规范，以生成真。(The本文档的第三部分通常作为策略生成的大纲证明呈现给人类读者，而不是策略本身。因此，重构工具应该能够转换声明、理论和策略.转换策略可以用来改进证明的结构它也可以用来泛化一个证明，这样这个策略仍然可以在重构的规范的上下文中证明定理。这意味着，除了规范的模式和重构之外，我们还需要策略的模式和重构。9.3为改进小的意义保持步骤，结合到更高级别的转换步骤，桥梁之间的差距，两种常见的证明风格。意义保持变换（例如[8]中的精化演算）的优点是步骤小，易于证明，但缺点是很难引导到期望的终点。假设和证明，用于Z细化的传统技术，具有能够找到所需终点的优点（它只是假设），但很难证明，因为步骤太大了。精化可以被认为是一种精化倾向于被铸造成一个应该利用重构的概念和适当的重构模式语言来构建一种方法，这种方法结合了小的、可证明的步骤的优点，以及达到期望的终点的优点689.4证明、重构、细化统一化总而言之：• 推理步骤将一个目标转换为具有相同含义的另一个目标战术语言将这些小步骤组合起来，产生大的推理步骤，旨在使目标更接近真实。• 重构将一个规范（声明、定理和策略）转换为另一个具有相同含义的规范重构语言将这些小步骤组合起来，产生大的转换步骤，旨在使规范更接近实现模式。• 精化把抽象的具体化转变为具有相同含义的具体化。精化重构语言可以将小的精化步骤组合起来，产生大的精化，旨在将抽象规范更接近实现。也就是说，所有这三个区域都可以被看作是意义保持变换的特殊情况。因此，目前在一个领域使用的技术很可能适用于其他两个领域。我们打算研究证明工具如何为精化工具和重构工具提供基础。10结论重构的代码更改原则已经同样富有成效地应用于许多大型商业正式规范和精化项目中的规范和证明维护。同样的重构原则也可以应用于规范升级。系统地结合重构和优化为规范维护和升级过程提供了一个结构。重构可以作为证明过程本身的一部分。证明和重构之间的类比可以扩展，以建议构建重构工具集和细化工具集的路线引用[1] 巴登河，S. Stepney和D.库珀，[2] Beck，K.，“Extreme Programming Explained,” Addison-Wesley,[3] Dyer，M.，《The Cleanroom Approach to Quality SoftwareDevelopment》，Wiley，1992年。[4] Fowler，M.，“Refactoring: improving the design of existing code,”Addison- Wesley,[5] 法兰西河B.（2002），（私人通信）。69[6] 伽 马 ， E. ， R. 赫 尔 姆 河 Johnson 和 J.Vlissides， “ 设 计 模 式 ” ， Addison-Wesley，1995年。[7] ISO/IEC 13568，[8] 摩根角，澳-地C.的方法，“Programming from Specifications,” Prentice Hall,[9] Stepney，S.，高完整性编译器的增量开发：工业开发的经验，第三届IEEE高保证系统工程研讨会（HASE'98），华盛顿特区，1998年[10] Stepney，S.，两个证明的故事，在：BCS-FACS第三北方正式方法研讨会，Ilkley（1998）。[11] Stepney ， S. 和 D. 库 珀 ， 工 业 产 品 的 形 式 方 法 ， 在 ： J.P.Bowen ， S 。Dunne ， A.Galloway 和 S.King ， editors ， ZB 2000 ： First InternationalConference of B and Z Users ， York ， August 2000 ， Lecture Notes inComputer Science1878（2000）.[12] Stepney，S.，D. Cooper和J. Woodcock，电子钱包：规范，改进和证明，技术专著PRG-126，编程研究小组，牛津大学计算实验室（2000年）。[13] Stepney，S.和F.Polack，A pattern language for Z，（in preparation）.
我的内容管理
展开
