重构的模型检查正确性

理论计算机科学电子笔记187（2007）3-17www.elsevier.com/locate/entcs重构的模型检查正确性-一些实验H.- Christian Estler，Thomas Ruhroth，Heike Wehrheim1InstitutfurInforormatikUniversitaütPaderborn n33098 Paderborn，Germany摘要重构是对程序、模型或规范所做的更改，目的是改进它们的结构，从而使它们更清晰、更可读和更可重用。重构必须是行为保持的，因为程序/模型/规范的外部行为保持不变。在本文中，我们将展示如何使用模型检查器（SAL）正式证明面向对象规范（用Object-Z编写）上的简单类型的重构是行为保持的。所处理的重构类仅涵盖那些对单个方法进行操作的重构类。关键词：重构，对象Z，模型检查，SAL1介绍重构是一种技术，程序员长期以来一直使用它来改善代码的结构，一旦它变得不可读。的博士Opdyke的论文[16]以及Fowler的书[11]使其流行起来，创造了术语重构是改变软件系统的过程，它不会改变代码的外部行为，但会改善其内部结构。在这里，结构的改进指的是面向对象的结构（即类层次结构），其方式与经典命令式程序的模块化相同。如今，重构是一种不仅应用于程序，而且还用于建模的技术，例如重构UML模型[21，17]或正式规范[12，13]。有关软件重构的调查，请参见[15]。1 电子邮件：{estler，thomas.ruhroth，wehrheim} @ uni-paderborn.de1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.08.0414H.- C. Estler等人/理论计算机科学电子笔记187（2007）3虽然“改善结构”是一个相当软的要求，通常是有争议的（什么是“好”的结构？），不改变外部行为的条件更精确。它应该保证代码或模型的用户，可能是人类或其他软件产品，可以像以前一样使用重构后的代码。这种变化应该是透明的。对于代码，行为保留通常在每次重构之后通过对代码的广泛测试来检查。在本文中，我们感兴趣的是形式规范上的重构。大型的正式（面向对象）规范在清晰性和良好结构性方面可能表现出与程序相同的缺陷。因此，重构也可以帮助改进规范的结构（或者为了以后的实现而修改结构）。虽然编程语言中的概念和形式规范中的概念之间没有一一对应的关系，但相似之处（显然）存在，并且福勒的一些重构在形式规范中有直接的我们感兴趣的规范语言是Object-Z [18]，它是基于状态的形式主义Z [22]的面向对象扩展。Object-Z规范的重构已经在[12，13，14]中讨论过了。在正式的环境中，行为保持的临界点可以被严格定义：细化[6，5]（或者甚至等价，即两个方向的细化）保证了期望的可替代程度。因此，数据细化（或者更准确地说，类细化）是在[13，14]中考虑的重构的正确性标准。虽然[13，14]定义了改变规范的面向对象结构（例如类层次结构）的重构，但在这里我们只处理仅对单个方法进行操作的重构（例如提取方法，简化条件，替换算法）。如果更改仅涉及一个方法，则行为保留的条件归结为检查重构前后方法定义的等效性这很容易导致重构前后类之间的细化关系。在（对象-）Z中，等价性可以通过应用谓词逻辑、集合论和Z的数学工具箱的规则来证明。然而，这样的证明通常是乏味的，而且经常容易出错（尽管它可以通过使用定理证明器来精确）。在这里，我们将使用模型检查器（SAL[3]）来显示等价性。我们的技术结合了[20，7]的思想，用于模型检查Z与SAL，[19] 将精化公式化为CTL模型检查问题。我们已经进行了一些实验，使用这种类型的等价性检查作为重构的正确性证明，在这里我们报告的结果。本文件的结构如下。我们从Object-Z类的一个小例子开始，在这个例子中我们说明了方法的四种不同的重构，并讨论了行为保留的概念。第3节将简要介绍SAL，并展示如何使用SAL检查重构的正确性最后一节总结并讨论了其他类型的重构，特别是关于它们所需的正确性的概念H.- C. Estler等人/理论计算机科学电子笔记187（2007）352重构示例重构是一种在不改变软件行为的情况下修改软件的方法。使用重构对于软件开发人员来说是很常见的，但是重构正式的规范也很有用。下面我们给出一个Object-Z规范的例子，并讨论它的一些重构。当将重构应用于规范或程序时，重构之间的结构差异可以很容易地看到。有些重构会在内部改变方法，而不改变类的其他组件。其他重构会改变类层次结构的一部分，而保持类在其范围之外不变。 因此，重构的分类可能会将其范围视为主要的区分标准。我们发现了四个重构操作的作用域• 方法，• 同学们，• 类层次结构，• 系统然而，这种严格的分类并不能总是保持，因为可能存在应用于方法的refac-torings，但仍然需要对规范的其余部分进行相应的更改（例如，重命名方法）。因此，方法重构可以进一步分为外部重构（随之而来的是对规范其余部分的更改这是后者，我们在本文中处理。作为我们重构的一个运行示例，我们使用图1中给出的桑拿房规范。类的第一部分是可见性列表。 这个列表声明了类的可见成员。这里列出的所有成员在类外都是可见的（就像Java中的public），否则它们在类外是不可见的（就像Java中的private/protected）。状态模式定义了一些变量和对变量的全局约束。在状态模式之后，有一个初始化模式（这里是开放的，因为它对重构没有特别的重要性）和一些操作模式。 我们有两个操作：updateControlLights和热量。 方法updateControlLights更新正确温度（clOk）、温度过热（clHot）和温度过冷（clCold）。如果当前温度与目标温度相差小于或等于2度，则认为温度正常，否则控制指示器分别设置为“太热”或“太冷”。如果桑拿房变冷，可以通过操作热加热。加热也改变了当前湿度。看看Sauna类，我们发现有些方法定义（特别是updateControlLights）不容易理解。接下来我们将根据一些重构规则来改变它们。在这里，我们对updateControlLights应用三种重构，对heat应用一种重构。重构的名称是根据Fowler书中的命名来选择的6H.- C. Estler等人/理论计算机科学电子笔记187（2007）3桑拿T（updateControlLights，heat，. . . ）目标温度：Z当前温度：Z关闭：BclCold：BclHot：B当前湿度：Z70≤目标温度≤ 100targetTempmod 5 = 060≤当前温度≤ 1000≤当前湿度≤ 100INIT.updateControlLightsΔ（clOk，clHot，clCold）currentTemp−targetTemp<−2℃（clOkJ=falseclHotJ= falseclColdJ = true）currentTemp−targetTemp>2℃（clOkJ= falseclHotJ = trueclColdJ = false）0≥currentTemp−targetTemp≥ − 2℃（clOkJ= true）0≤currentTemp−targetTemp≤ 2℃（clOkJ=trueclHotJ= falseclColdJ = false）热Δ（当前湿度，当前温度）currentTemp≤targetTemp+2currentTempJ=currentTemp+2currentHumidityJ=currentTempJ div 5.Fig. 1. 样本类别：桑拿引入解释变量第一次重构利用了表达式currentTemp−targetTemp在updateControlLights的谓词中重复出现的事实。 我们应用重构规则”[11]他说：“你有一个复杂的表达。把结果H.- C. Estler等人/理论计算机科学电子笔记187（2007）37updateControlLightsIEVΔ（clOk，clHot，clCold）温度：Z·温度=当前温度−目标温度diff<−2⇒（clOkJ=falseclHotJ= falseclColdJ = true）2、2、（clOkJ=falseclHotJ= trueclColdJ = false）0≤d1≤2（clOkJ=trueclHotJ=falseclColdJ= false）0≥di≥ −2（clOkJ=trueclHotJ= falseclColdJ = false）在临时变量中的表达式或表达式的一部分，该临时变量的名称解释了其用途。在这里，我们引入了新的变量di。引入一个新的变量是通过一个存在量化器来表示的。按功能重构循环表达式的另一种方法是应用“Consolidate Condition”。而不是使用一个额外的变量，我们使用函数来表达条件。Fowler说：“你有一系列条件测试，结果都是一样的。将它们组合成一个条件表达式并提取它。绝对值：Z→ Nx0abs（x）=−x x≥0abs（x）=x<温度：Z× Z›→ Zn，m：Z·tempdi n（m，n）=m-n更新控制灯CCFΔ（clOk，clHot，clCold）tempdi（currentTemp，targetTemp）<−2（clOkJ=falseclHotJ= falseclColdJ = true）tempdi（currentTemp，targetTemp）>2℃（clOkJ=falseclHotJ= trueclColdJ = false）abs（tempdi（currentTemp，targetTemp））≤2℃（clOkJ=trueclHotJ= falseclColdJ = false）在这个例子中，我们引入了两个新函数（abs和tempdi）。然后在谓词中使用这些。8H.- C. Estler等人/理论计算机科学电子笔记187（2007）3.加热试验Δ（当前温度）currentTemp≤targetTemp+2currentTempJ=currentTemp+2希思Δ（当前湿度）currentHumidityJ=currentTemp div 5heat=^heatToheat H9.updateControlLightsSAeΔ（clOk，clHot，clCold）clColdJ=currentTemp≤targetTemp−2clHotJ=currentTemp≥targetTemp+2clOkJ=2≥currentTemp−targetTemp≥ − 2替代算法到目前为止使用的所有版本的updateControlLights仍然是冗长的。下一次重构将改变这一点。我们不是测试温度范围和调整所有灯，而是为每个灯定义温度范围并单独调整每个灯。因此，updateControlLights被一个全新的定义（updateControlLightsSA）所取代。这是重构“替代算法”的一个应用。提取方法最 后 ， 我 们 来 看 看 方 法 的 热 度 。 该 方 法 调 整 currentTemp 和currentHumidity。这现在被分成两个新的方法，然后通过顺序组合（重构“提取方法”的特殊情况）进行组合Δ-列表被修剪以仅适合修改后的变量。由于新操作不在可见性列表中，因此无法直接从其他类调用它们桑拿在执行了这些重构之后，我们最终必须确保这些都是行为保持的。为此，我们首先必须定义内部方法重构的行为保持。我们的目的是得到与旧方法相当的方法。因此，重构后的类和原始类将是彼此的细化。H.- C. Estler等人/理论计算机科学电子笔记187（2007）39Let（State，Init，（Opi）i∈I）是所有类的最优集合，并且d（State，Init，（Opi）i∈I\{j}，Opi）是所有类的最优集合。这些因素会导致操作中断。MethodOpsequivalettomethodOpjJ J如果以下两个条件成立：(1) State·preOpj惠preO(2) State，StateJ·Opj惠O条件（1）是细化的适用性规则的类比，规则2是正确性规则。这两个都只需要检查重构的方法。3检查正确性在本节中，我们将展示如何确保上一节中给出的重构在上述定义的意义上是行为保持的。为此，我们将我们的Object-Z模式转换成SAL语言，并使用SAL的CTL模型检查器验证方法的等价性。我们下面的翻译和验证方法是基于[19]和[20]中描述的思想。3.1SAL符号分析实验室（SAL）[3]由SRI International的形式方法计划开发。它是一个框架，结合了不同的工具，用于程序分析，定理证明和状态转换系统的模型检查。目前SAL提供了四种不同的模型检查器，其中一种用于检查CTL属性[9]，一个模拟器和一些其他工具，它们都工作在同一种输入语言上，称为SAL语言。SAL语言是作为一种中间语言开发的，作为高级语言（如Java）翻译器的目标平台。 因此，它支持一个广泛的类型定义和表达式。 然而，SAL语言也可以用来描述过渡系统本身。它与SMV、Murphi或SPIN等验证工具使用的语言没有什么不同。SAL语言的完整规范可以在SAL语言手册中找到[4]。在这一点上，我们介绍了一些必要的基本结构来理解我们的Z规范的SAL编码。上下文所有SAL输入（如声明、模块或定理）都在一个上下文中分组。我们考虑对桑拿浴规范进行翻译，以说明SAL语言结构。桑拿：上下文=开始Int：TYPE =[-100.. 100]; %我们自己的整数类型Nat：TYPE =[0.. 100];%我们自己的自然类型neg（n：Nat）：Int =-n; %函数对n取反尚未在上下文main：MOST = BEGIN目标温度，当前温度：Int10H.- C. Estler等人/理论计算机科学电子笔记187（2007）3clclOk，clCold，clHot：布尔电流湿度：IntINVAR：布尔定义Invar =（70 = targetTemp）AND（targetTemp = 100）AND（targetTempMOD 5 = 0）AND(60= currentTemp）AND（currentTemp = 100）AND（0 =当前湿度）和（当前湿度= 100）初始化[因瓦--> targetTemp IN {i：Int| TRUE};currentTemp IN {i：Int|TRUE}; clCold IN {b：布尔|TRUE}; clHot IN {b：布尔|TRUE}; clOk IN {b：布尔|};currentHumidityIN {i：Int|真}]过渡期[updateCL：（当前温度-目标温度-2）=>（clOk（currentTemp- targetTemp >-2）=>（clOk（0>= currentTemp- targetTemp）AND（currentTemp- targetTemp>=-2）=>（clOk（0 = currentTemp- targetTemp）AND（currentTemp- targetTemp = 2）=>（clOk因瓦--> clCold ' IN {b：布尔|TRUE}; clHot' IN{b：布尔|TRUE}; clOk ' IN {b：布尔|真}[]加热：[]（currentTemp = targetTemp + 2）AND（currentTemp--> currentTemp' IN {i：Int| TRUE};currentHumidity' IN {i：Int|真}否则-->]END;END注释以%符号开头，并以行尾结束。 SAL语言区分大小写，保留字（如CONTEXT、BEGIN和END）用大写字母书写。在下文中，我们将逐步解释SAL规范的各个部分。宣言SAL支持内置的基本类型，如BOOLEAN，NATURAL，INTEGER或REAL。 所有这些都可以与SAL工具箱的无限有界模型检查器一起使用。但是，由于CTL模型检查器工作在有限类型上，我们必须通过以Name>的形式实现它们来声明我们自己的类型<：<类型>。 定义一个新的类型我们使用下面的结构：Type>= Expression>，它也可以用来表达功能。在我们的例子中，我们定义了我们自己的自然和整数类型（Int，Nat）以及一个函数来否定自然数。模块一个模块基本上描述了一个状态转换系统。它由变量组成，可以是INPUT、GLOBAL 或 OUTPUT 。 不 变 量 在 DEFINITION 部 分 描 述 ， 初 始 值 在INITIALIZATION部分声明，H.- C. Estler等人/理论计算机科学电子笔记187（2007）311转换函数由关键字TRANSITION标记。对于单个转换函数，我们始终使用由以下内容组成的保护命令 一个警卫和一个任务。守卫−− >分配SAL非确定性地为赋值中给定的变量选择值，让我们考虑下面的例子：当前温度60--> currentTemp这个受保护的命令只不过是一个如果。然后是表情。我们可以重新输入为currentTemp更有趣的是像58 = currentTemp--> currentTemp' IN {i：Int|真}如果执行具有这样的命令的转换，我们得到5个后继状态，其中currentTemp的值在58和62之间。因此，受保护的命令是比简单的if.更强大的结构。然后是表达式。如[20]中所述，我们使用它们作为将Z模式的谓词编码为SAL的通用方法。最后，应该注意我们示例中最后一个被保护的命令ELSE -->。为了从模型检查器中得到正确的结果，转换关系必须是完全的，这样模块就不会死锁。这个特殊如果所有其他防护评估为假，则防护评估为真，并保持状态不变。公式在SAL规范上检查的属性必须写入它们所引用的模块下面的- orems中。例如，th 1：THEOREM main|-AG（EX（clOk = TRUE））;定义一个名为th 1的定理，该定理陈述如下：属性（在CTL [9]中给出）：在所有执行路径上，每个状态都有一个clOk为true的下一个状态。3.2使用SAL的G. Smith和J.Derrick已经展示了如何使用SAL模型检查器和模拟规则的CTL编码来验证Z规范的数据细化[19]。我们对Object-Z规范的重构只适用于简单的方法，而不是面向对象的结构，因此我们可以重用这种技术来检查方法的等价性。12H.- C. Estler等人/理论计算机科学电子笔记187（2007）3正如上一节所定义的，我们需要证明一个适用性和一个正确性条件。 基本上，这意味着我们必须验证我们的原始-在所有S=（State，Init，（Opi）i∈I）的情况下，S^=（State，Init，（Opi）i∈I\{j}，Oppj），其中具有根据所述条件重新生成Oppj的条件同样的方式。像sal-wmc这样的符号模型检查器构建了一个表示所有可达状态的Kripke结构的符号直观的想法可以是分别在给定任意的操作序列的情况下，将S和S_A的结构分别提供为简单的结构。但是，由于模型检查器没有被设计为将独立的数据集合并到一个系统中，因此我们需要将S和S^in合并到一个系统中，并以这样一种方式定义这个合并的系统，即我们实际上可以验证适用性和正确性。下面的技术基本上是基于[19]。起点是我们原始类的SAL规范。在第一步中，我们必须解决CTL不允许命题引用操作的问题。因此，我们通过变量ev增加State：Exp。此外，我们通过evJ=Opi来增加每个操作Opi，使得ev给我们唯一的信息哪个操作导致了实际状态。 为了确保转换关系是total 我 们引 入了 另一 个操 作 Choose ， 它 总是 启用 并选 择一 个新 的状 态（Choose替换了ELSE -->guard）。因此，我们通过比较State：E xp：S^tate（因为我们需要将旧方法的效果与新方法的效果进行比较）来确定所有的y x t en d o r s y s s y s t e m。对于State中的每个variabl e x：E x pwdeclar e anwariabl e x^。ThereefactoredoperationOpj现在，为了实现这种性能，它的平均值为J=Opi，并且在工作时进行了修改x^anddx^JinsteadoffxanddxJ. 对于我们来说，对于我们的公司来说，将状态变量的副本与原始版本相关联。为此我们在R^re中定义一个r el at i a ti Rcannbeseenasom e州，州^这种检索关系构成了State：Exp与State的同一性。最后，我们修正了这个组合系统的初始化：它被设置为任何可能的其中，R为真。我们有意识地忽略任何预设声称，赢了赢了Object-Z规范中的Init，因为Init为true的状态集是一个子集R为真的状态的集合 在本SAL规范中，以下两个CTL公式可用于检查新旧方法的等效性：适用性检查：正确性检查：EX（ev=Opj）惠EX（ev=Opj）AX（ev=OpjEX（ev=OpR^））j州，州∧AX（ev=OpEX（ev=OpR^））j j州，州H.- C. Estler等人/理论计算机科学电子笔记187（2007）313updateControlLightsIEVΔ（clOk，clHot，clCold）温度范围：Z·温度范围=当前温度−目标温度范围<−公差温度范围（clOkJ=falseclHotJ= falseclColdJ = true）.第一个公式指出，当且仅当新操作可以在状态的相应副本中执行时，旧操作可以在状态中执行。 正确性的两个公式指出，每当旧方法被执行从而修改状态时，新方法的执行也可能导致等价的（在R下）状态，反之亦然，新旧颠倒。我们在这里得到两个公式（而不是一个用于细化的公式），因为我们想要等价而不仅仅是一个蕴涵。既然我们现在知道如何验证我们的重构，我们将更仔细地研究它们到SAL语言的翻译3.2.1引入解释变量我们的第一次重构引入了新的变量di。SAL语言支持quanti fier和quantifier，因此这种方法的翻译很简单。我们只需要考虑quantifier的作用域覆盖了整个谓词。这是通过将整个表达式括起来来确保的updateControlLightsIEV：（EXISTS（diff：Int）：diff= currentTemp_N-targetTemp_NAND（（diff = neg（toleranceTemp_N）=>（clOk_N（（diff>= toleranceTemp_N）=>（clOk_N((0<=diff）AND（diff<= toleranceTemp_N）=>（clOk_N((0>=diff）AND（diff>= neg（toleranceTemp_N））=>（clOk_N(ev’ =--> clCold_N ' IN {b：布尔|TRUE}; clHot_N'IN {b：布尔|TRUE}; clOk_N ' IN {b：布尔|TRUE}; ev' IN {ev：EVENT|真}当我们采用此规范并使用上述方案验证新旧方法的等效性时，SAL返回肯定的答案。因此，这种重构是行为保留的。3.2.2按功能我们定义了两个新函数tempdi和abs，以简化我们的规范。14H.- C. Estler等人/理论计算机科学电子笔记187（2007）3updateControlLightsSAoΔ（clOk，clHot，clCold）clColdJ=currentTemptargetTemp− 2clHotJ=currentTemp>targetTemp+2clOkJ=2≥currentTemp−targetTemp≥ − 2<绝对值：Z→ Nx0abs（x）=−x x≥0abs（x）=x<温度：Z× Z›→ Zn，m：Z·tempdi n（m，n）=m-n一开始，我们已经看到函数可以在上下文中实现。译文如下：abs（i：Int）：NATURAL =IFi 0 THEN-i ELSEi ENDIF;tempdiff（n：Int，m：Int）：Int= n-m;到目前为止，这些函数可以在方法中用于更新控件。updateControlLightsCCF：（（tempdiff（currentTemp_N，targetTemp_N）=neg（toleranceTemp_N））=>（clOk_N...同样，SAL3.2.3替代算法接下来，我们尝试验证updateControlLights及其重构updateControlLightsSAe之间的相等性。在这种情况下，验证失败，SAL告诉我们正确性定理是无效的。关于模型检查器创建的反例，我们发现updateControlLightsSAe允许打开多个灯，这在以前是不可能的。 因此，新旧方法实际上是不等价的。因此，我们必须纠正 我 们 的 重 构 ， 并 将 我 们 模 块 中 的 updateControlLightSAe 替 换 为updateControlLightSAo的翻译，这次成功地证明了等价性。即使这只是一个很小的例子，而且在仔细检查时可能会发现错误，它也证明了模型检查是一种有效的调试重构的方法。3.2.4Split方法最后，我们来看看热量的分解。SAL并没有为我们提供一个等同于顺序模式组合的操作符。因此，我们必须找到另一种翻译方法。记住Z和SAL之间自动翻译的一般思想，应用组合的定义是有意义的。根据[22]，两个模式S和T的组合可以描述为：H.- C. Estler等人/理论计算机科学电子笔记187（2007）3159如下所示：SoT=StateJJ·S[StateJJ/StateJ]T[StateJJ/State]使用这个定义，我们可以对重构进行编码并验证等价性。合并在重构过程中分离的两个方法可能会让人感到恼火。然而，我们不能忘记，这只是Z和SAL之间翻译的结果。想象一下，一个为任何Object-Z规范创建正确SAL代码的工具，它将向我们揭示内部方法重构中的任何失败。4讨论和结论在本文中，我们研究了使用模型检查器来证明重构的我们看到的重构类是那些只改变一个方法的重构类。除了清理方法的规范之外，这些重构通常也是更大重构的先决条件，例如Pull方法或引入继承，仅当方法不同的类是等价的。一般来说，重构的行为保留的自动检查因此是一个有用的工具。由于我们处理的是单个方法，并且只考虑重构改进其内部结构，行为保持的形式含义很容易回答：行为保持是方法等价（或双向数据细化）。然而，这并不适用于所有Fowler的重构。事实上，当孤立地看待单个类时，大量的重构可以立即被视为不是标准的重构。例如，这适用于所有改变方法参数的重构（可以发现这是一种IO-细化[1]），将方法拆分为许多其他方法的重构（非原子细化[8]）或添加新方法的重构（行为子类型[10]）。与我们在这里研究的简单方法等价不同，这些重构对其他类有影响：类的接口改变了，因此使用这些方法的所有其他类也必须改变。因此，行为保留的检查可能必须涉及规范的更大部分;然后要检查的是类细化，将Object-Z规范的一个特定类作为“主”类，并显示该类的等价性和/或细化。在未来，我们打算研究这些类型的重构和检查其正确性的方法作为模型检验方法等价性的工具，我们在这里选择了SAL。SAL自Z到SAL的翻译最近被给出以来，就把自己作为一种工具来使用。选择使用模型检查器（而不是定理证明器）进行等价性检查的动机是希望获得自动正确性检查。然而，这限制了该技术对有限（而且通常很小）数据域的规范的适用性。除了这些模型检查的标准限制在重构过程中，在其他方法中使用方法是很常见的。但是，SAL不允许在其他转换的定义中使用转换名称因此，大多数时候，16H.- C. Estler等人/理论计算机科学电子笔记187（2007）3这些定义必须在转换为SAL期间扩展，因此重构丢失。这也适用于一些改变数据类型的重构：不同的Z类型可能映射到相同的SAL类型上，因此重构可能在转换过程中已经消失。作为未来的工作，我们还打算使用Alloy来检查重构的行为保留。合金比SAL更接近Z，因此可能为检查等效性开辟新的可能性。Bolton [2]使用Alloy来验证精化，她的工作可以作为检查等价性的起点确认我们感谢Graeme Smith和John Derrick为我们提供了用于Z的数学工具包的SAL库。这项工作的部分资金由德国研究委员会DFG在赠款WE 2290/6-1。引用[1] E. A. Boiten和J. Derrick。 Z中的IO修饰。 以. 埃文斯，D. J. Duke和T. 克拉克，编辑，第三次BCS-FACS北方正式方法研讨会。Springer-Verlag，1998年9月。http://www.ewic.org.uk/的网站。[2] C.博尔顿使用合金分析仪验证Z中的数据细化。在2005年的《理论计算机科学中的电子笔记》中。[3] L. de Bagio，S. 奥雷Rue，J. Rushby，N.尚卡尔，M。Sorea和A. 蒂瓦里 Sal 2. In R. Alzheimer和D.Peled，编辑，计算机辅助验证国际会议（CAV 2004），LNCS第3114号，第496-500页。Springer-Verlag，2004.[4] L. de Bagio，S. Owre和N.史恩卡 SAL语言手册，2003年。[5] W.- P. de Roever和K.恩格尔哈特数据精炼：面向模型的证明方法及其比较。CUP，1998年。[6] J. Derrick和E.A. 煮一下Z和Object-Z中的细化。Springer-Verlag，2001.[7] J. Derrick，S. North和T.西蒙斯实现Z.在ICFEM 2006年，LNCS。施普林格，2006年。出现。[8] J. Derrick和H.维海姆在非原子细化中使用耦合模拟。ZB2003：Z和B的正式规范和开发，LNCS第2651号，第127Springer，2003年。[9] E.A.爱默生和E.M.克拉克使用分支时间时序逻辑来合成同步骨架。Science of Computer Programming，2（3）：241[10] C. Fischer 和 H. 维 海 姆 面 向 对 象 形 式 体 系 的 行 为 子 类 型 关 系 。 于 T. Rus ， editor ， AMAST 2000 ：International Conference on Algesthetics Methodology And Software Technology，number 1816，pages 469斯普林格，2000年。[11]M.福勒重构：改进现有代码的设计。艾迪森·韦斯利2004年[12] T. 麦库姆重构Object-Z规范。软件工程的基本方法（FASESpringer，2004.[13] T. McComb和G.史密斯Object-Z中的建筑设计。澳大利亚软件工程会议（ASWECIEEE ComputerSociety Press，2004.[14] T. McComb和G.史密斯重构面向对象规范：一个派生设计的过程。技术报告SSE-2006-01，澳大利亚昆士兰大学信息技术与电气工程学院，2006年5月。H.- C. Estler等人/理论计算机科学电子笔记187（2007）317[15] T.我 和 T 。你也是 。一 份 关 于 Softwa reRefactoring 的 综 述 。IEEETransactionson SoftwareEngineering，30（2），2004.[16] W.F.奥普代克重构：设计面向对象应用程序框架的程序重构辅助工具。博士论文，伊利诺伊大学香槟分校，1992年。[17]J. Philipps和B.朗普重构程序和规范，第281-297页。 Kluwer Academic Publishers，2003.[18] G.史密斯 Object-Z Specification Language。 Kluwer学术出版社，2000年。[19] G.史密斯和J.德里克。使用模型检查器检查数据修正。Formal Aspects of Computing，2006.地出现。[20] G.史密斯和L.怀尔德曼 使用SAL对Z规范进行模型检查。 在我店国际会议B和Z用户（ZB 2005），计算机科学讲义第3455卷，第85-103页。Springer-Verlag，2005.[21] 我是苏尼耶，达米恩·波莱特，伊韦斯·勒·特拉翁，还有让-马克·杰·泽·奎尔。 R ef actori ngUML模型。MartinGogolla和Cris Kobryn，编辑，UML 2001 -统一建模语言。建模语言、概念和工具。第四届国际会议，加拿大多伦多，2001年10月，会议记录，LNCS第2185卷，第134-148页。Springer，2001年。[22] J. C.伍德考克和戴维斯。 使用Z：规格化，细化和证明。 Prentice Hall，1996年。