理论计算机科学电子笔记：使用解释函数进行证明转换及其在软件工程中的应用.

理论计算机科学电子笔记127（2005）139-145www.elsevier.com/locate/entcs通过解释函数进行证明转换：结果、问题和应用彼得·科修琴科莱斯特大学计算机科学系英国莱斯特摘要变更是软件工程过程中一个不变的因素。类结构的重新设计需要转换相应的OCL约束。 在以前的论文中，我们已经展示了如何 使用我们所谓的解释函数来转换约束。在本文中，我们讨论最近获得的结果证明变换通过这样的功能。特别是，我们详细说明了这样一个事实，即他们保持证明方程逻辑，以及证明在其他逻辑系统，如命题逻辑与肯定前件或证明使用决议规则。这些结果对UML状态机和序列图的重新设计有直接的应用。如果状态机中的状态由状态不变量来解释，则其状态之间的拓扑关系可以被解释为相应公式之间的逻辑关系。结果关系的保持可以看作是状态机拓扑的保持。我们还指出了一个未解决的问题，并讨论了挖掘其正解。关键词：UML，重新设计，证明转换，约束转换，状态机，序列图，形式化方法。1介绍统一建模语言为系统规范提供了文本和图形方法（参见[13]）。系统及其现实世界的环境使用抽象建模，如类图，状态机或序列图。有不同的软件工程过程，1 该研究部分由欧盟项目Leg2Net和欧盟项目AGILE资助。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.08.040140P. Kosiuczenko/电子笔记理论计算机科学127（2005）139可以应用。在老式的瀑布模型中，人们必须从正确的需求规格开始，进行改进以获得设计，然后实现设计规格。这些步骤可以用细化的概念来充分描述（参见 例如[8]）。 如果需求没有改变，并且软件开发人员对如何继续有一个清晰的想法，那么这就可以正常工作。然而，实际上，由于多种因素，包括客户需求的变化或新的需求、新的技术推动因素等，规格会不断变化。在这种情况下，需要对系统规格和设计进行大量的手动重新设计。今天在这种情况下，需求跟踪就更难实现了。具有单调性假设的细化概念几乎不能模拟这种变化。例如，如果一个接口或类的签名发生了变化，那么描述与实现该接口的类相关的属性的公式或约束可能不再有意义。市场上没有工具允许自动转换约束。必须手动更改规范，这非常耗时且容易出错。已经存在许多重新设计UML类模型的方法。最著名的是重构方法[1]。它为代码和类结构修改提供了简单的模式在抽象代数中使用的解释函数[11]将单个运算转换为复数项。图重写系统可以用于转换规范（参见图1）。例如[3]）。在以前的文章[8]（也可参见[5]）中，我们研究了带OCL约束的UML状态不变量的重新设计，以及约束的 我们引入了一个新的解释函数的概念来重新设计状态不变量，它以一种自然的方式扩展了[ 11 ]中引入的概念;解释函数是由满足类似于项重写系统中的正交性的条件的映射生成的合成函数。我们重新设计的概念比细化的概念更一般，因为我们不假设属性只是添加或细化，而是允许以任意方式改变它们。例如，许多设计级别类可能会被重新构造，或者一个规范级别类可能会被分成几个设计级别类。必须预先提供的属性可能涉及类、关联、属性或泛化关系之间的依赖关系。它们用OCL公式表示，并进行了变换.我们的方法是由抽象的概念，因为它是在UML中使用的动机[13]。有趣的是，我们的方法不仅允许我们进行自动约束转换，还允许进行自动证明转换。在技术报告[6]中，我们已经证明了几种蕴涵关系，P. Kosiuczenko/电子笔记理论计算机科学127（2005）139141通过解释函数来保存公式;特别地，这样的函数保存等式证明、使用命题重言式的证明、归结规则和归纳。这使得一个人可以在转换类图之后节省重新做证明的文书工作本文简要介绍了技术报告中的结果[5]并讨论了它们在状态机和序列图的重新设计中的应用。在第二节中，我们简要地介绍了解释函数的概念和相应的结果。在第3节中，我们将展示如何将此思想和结果应用于状态机和序列图的重新设计。在第四部分中，我们总结了本文的研究，并列出了一些有待解决的问题。2口译职能解释函数被证明是非常有用的，当对类图进行更改时，它可以作为OCL约束自动转换的工具[6]（另见[4]）。例如，如果类型为Integer的属性a被路径b替换。x，其中b是指向另一个类的关联，x是该类的属性，那么每个包含a的OCL约束或状态不变量都必须修改。这种修改可以使用解释函数来执行即由满足类似于正交项重写系统的条件的映射生成的部分函数（参见，例如[12]）。这种映射的一个域满足对正交项重写系统的所有域有效的条件即域中的所有项都是线性的并且不重叠。解释函数有几个有用的属性。它们允许我们转换OCL规范。其思想是，改变类结构的设计者或实现者将修改后的模型元素映射到目标模型元素上，相应约束的转换自动完成。这样的功能保持方程的证明，证明使用命题重言式，决议规则和证明归纳[5]。这使得人们可以在转换类图之后节省重新进行这种证明的文书工作。3应用有趣的是，结果有关保留的后果关系也有在下面的三个小节中，我们考虑将我们的概念应用于状态机和序列图。142P. Kosiuczenko/电子笔记理论计算机科学127（2005）1393.1状态机最有用的UML图之一是所谓的状态机[13]。一个状态机是由多个状态组成的，这些状态由对应于转换的边连接起来。状态可以是结构化的;一个状态可以包含几个其他的状态，称为子状态。在UML中，因此，状态机中的状态对应于公式;在第一种情况下，公式被称为状态不变量。这样的公式可以描述对象属性的值和不同对象之间的相互关系;它们可以例如在OCL中表示状态机的状态可以用树来表示，特别是用命题公式来表示（参见。[9]）。我们认为，状态机中状态之间的拓扑关系在这种情况下，蕴涵关系的保持可以被视为状态机的拓扑的保持。假设对应于子状态的不变量隐含对应于其超状态的不变量是很自然的，因为对应于子状态的不变量应该更具限制性。这个条件（我们称之为状态单调性）可以正式表示如下：对于每两个状态s1和s2，s1是s2的子状态当且仅当对应于s1的公式蕴涵对应于s2的公式。另一方面，如果一个国家机器的状态涵盖了所有的可能性，人们可能会感兴趣。在状态机描述对象行为的情况下，这意味着对于对象属性的每个组合，都有一个状态覆盖该组合。当状态由不变量解释时，这种覆盖属性可以等价地表示为对于属性的每个组合，存在描述该组合的状态不变量的要求。形式上，设F i，其中i = 1，.，n是对应于状态机M的所有状态的公式;M的状态覆盖所有可能性当且仅当公式F1满足. 是一种互变函数。Equivalent，F1... 可以证明，而不使用域特定的公式。一个更强的性质（我们称之为穷尽性）说，对于每一个所谓的或态，它的所有子态都覆盖了所有的可能性。形式上，让s是一个或状态，让F是相应的状态不变量，让s1，.，s n是s的所有子状态，设F1，.，Fn是相应的不变量。F是穷举的，当且仅当如果F在逻辑上等价于析取式F1. [医]真菌;真菌我们说国家在状态机中，如果对于或状态s的每两个不同的子状态s1和s2，F1→F2在逻辑上是假的。P. Kosiuczenko/电子笔记理论计算机科学127（2005）139143还有其他几个有用的性质，这类性质可以用公式之间的逻辑关系来表示。例如，所有可达状态都由非矛盾公式定义，或者对应于正交状态的公式的析取等价于超态不变量（类似于穷举的条件）。如上所述，类图的转换需要转换相应的约束（例如OCL约束）。因此，如果状态机的状态由公式描述，则可能需要改变那些公式如果一阶逻辑中的蕴涵被解释函数保持，那么上述所有性质都被这样的函数保持。文献[5]的结果表明，解释函数保持了使用等式推理、归结规则、命题重言式和归纳法的证明因此，目前我们可以说，如果上述性质是使用这些类型的推理证明，那么它们是由解释函数保持的。例如，如果存在使用上述推理方式的状态单调性性质的证明，则在经由解释函数的变换之后，该性质在变换之后保持有效。3.2序列图UML 2.0为序列图（SD）引入了条件[14]。它们不像状态机中的状态不变量那样发挥核心作用。另一方面，SD中的结构化机制是不同类型的;这些是对轨迹集的操作，以促进行为规范。上一节包含了一个可以用逻辑术语定义的状态机属性列表。以类似的方式，可以定义序列图的属性在这种情况下，这些约束关系到跟踪规范的组成例如，可以要求使用并行组合获得的序列图中的条件是不矛盾的，或者通过替代组合组合的序列图具有排他性的先决条件。与状态机的情况一样，逻辑结果的保持意味着这些属性由解释函数保持4结束语和今后的工作本文证明了文[6]和文[5]中的结果对UML图的转换，特别是对状态机和顺序图的转换有直接的我们表明，在一个状态机的状态不变量，蚂蚁之间的逻辑关系被保存，如果它们可以被证明使用某种证明。144P. Kosiuczenko/电子笔记理论计算机科学127（2005）139仍有几个悬而未决的问题。特别是，不知道解释函数是否保持一阶逻辑的蕴涵关系。这个问题可能看起来纯粹是理论性的，但是一个肯定的答案会对状态机和序列图产生非常有趣的影响;例如，它意味着解释函数保持状态机的拓扑结构。即使答案是否定的，迄今为止取得的结果也证明是有用的。在未来，我们将进一步研究解释功能的逻辑术语的性质。我们将研究一阶逻辑的蕴涵关系是否被解释函数保持。在第一阶逻辑中，语义结果和句法结果是等价的到目前为止，我们得到的结果主要集中在句法上。机构从模型论的观点来探讨转换问题（参见。例如[10]）。我们将研究解释功能与制度的关系。我们还计划实现一个工具，支持类的重新设计，转换和模型元素的跟踪。这样的工具将是非常有帮助的，因为复杂的OCL约束的纯手动转换非常费力且容易出错。引用[1] Fowler，M.，重构：改进现有代码的设计，阅读，马萨诸塞州，艾迪生-韦斯利出版社，2000年.[2] 伽马，E.，赫尔姆河，约翰逊河，Vlissides，Design Patterns，Addison-Wesley，Reading，1995。[3] Grosse-Rhode ， M. ， 和 Presicce ， F. ， 和 M. Simeoni ， Formal software specification withrefinements and modules of typed graph transformation systems，Journal of Computer andSystem Sciences，64（2），2002。[4] Kosiuczenko，P.，UML类图的形式化重新设计，在（Evans，A.，法国河，Moreira，A.，朗普湾Eds）：Proc. of pUML Workshop on Practical UML Based Rigorous Development Methods，Toronto. GI版，信息学讲义，2001年。[5] Kosiuczenko，P.，通过解释功能进行证明转换，技术报告编号。2004/27，莱斯特大学，2004年，16页：http://www.cs.le.ac.uk/~pk82/Theory1.1.pdf。[6] Kosiuczenko，P.，Redesign of UML Class Diagrams：a formal Approach，2004年出版。[7] Kosiuczenko，P.，通过解释函数的证明转换：结果，问题和应用，将出现在ENTCS，2004年。[8] Lano，K.，面向对象的形式化开发，Springer，柏林，1995。[9] Luét gen，G. ，和M. 《网络经济中的经济与科学》，载《地理信息系统/OCG-Jahrest a gung》，K. Bauknecht，W. 我的天啊。 Muck（eds. ），Viena，25.09.2001。P. Kosiuczenko/电子笔记理论计算机科学127（2005）139145[10] Tarlecki，A.，机构：正式规范的抽象框架，在（Astesiano，E.，Kreowski，H. -J. ，Kr ieg-Bru？ckn e r，B. Ed s。）：AlgebraicFondationsofSystemSpecication，Springer，1999年。[11] 泰勒，W.，Characterizing Malcev conditions，Algebra Universalis，3，Springer，Berlin，1973，351-397.[12] Terese et.例如， 术语重写系统，剑桥大学出版社，2003年。[13] OMG，统一建模语言规范，1.5版，2003年。[14] OMG，统一建模语言规范，2.0版（待定），2004。