可在www.sciencedirect.com在线获取理论计算机科学电子笔记304（2014）81-96www.elsevier.com/locate/entcsOCL的K语义安德烈·阿鲁索艾·多雷尔·卢卡努罗马尼亚亚速尔大学计算机科学系弗拉德·鲁苏Inria Lille Nord EuropeVilleneuve摘要我们给出了一个形式定义的一个重要子集的对象约束语言（ocL）在K框架.选择的子集包括常用的算术、布尔（包括量化器）和字符串表达式;集合表达式（包括迭代器和导航）;以及方法的前/后条件由于是可执行的，我们的定义免费为我们提供了一个用于所选ocL子集的解释器。它可以免费使用在K定义的语言有ocL作为一个组成部分我们说明了一些优势，K通过比较我们的语义定义ocL与语言的标准的专业语义我们还报告了一个实现我们定义的工具，用户可以在线尝试关键词：对象约束语言，形式化可执行语义，K语义框架1介绍对象约束语言（OCL）是一种用于在UML模型上编写约束的文本语言它是在90年代中期由ibm设计的，并从uml1.1版开始被纳入umlOCL旨在成为一种正式的规范语言。它被用来增加uml模型所缺乏的精确度。它的OMG标准[15]定义了语言的语法，在某种程度上，它的语义。然而，尽管有许多关于ocl的学术著作（其中一些在相关著作部分中被引用），但目前还没有一个商业工具可以完全支持它。1电子邮件：andrei. gmail.com2电子邮件：dlucanu@info.uaic.ro3电子邮件：Vlad. inria.frhttp://dx.doi.org/10.1016/j.entcs.2014.05.0041571-0661/© 2014 Elsevier B. V.保留所有权利。82A. Arusoaie et al. /Electronic Notes in Theoretical Computer Science 304（2014）81- -部分问题在于标准，它不精确，不完整，在某些地方令人敬畏。这对于许多语言来说是常见的，对于这些语言，语义在声明为标准的手册中被非正式地描述（参见，例如，C的定义[9]。其中一些问题包括从无序到有序集合和包的不确定性转换操作，单例集合a和集合元素a是否应该是不同的问题（在标准的不同页面中有不同的回答[15]），以及由于存在无效值而引起的问题。在本文中，我们报告了在K框架[22]中对ocl的正式语义进行的工作。K是一个语义框架，主要用于定义编程语言的正式操作语义K语义是可执行的，这意味着用定义的语言编写的程序可以被执行、测试，并在不久的将来被正式验证。我们已经定义了OCL的静态部分（对应于UML模型上的良构约束和查询）和动态部分（对应于方法的此外，我们允许在符号模型上评估ocl表达式模型，其属性可以具有符号值5.例如，这允许我们计算满足给定OCL约束的符号模型的具体实例存在的条件（关于变量）;并计算给定方法调用序列可行的条件。然后，这些条件可以传递给约束求解器，以检查它们是否满足。一个否定的答案对用户来说是一个有用的反馈：他们需要修改他们的模型和ocl表达式，以便使它们彼此一致关于静态部分，定义的ocl片段由通常的算术、布尔（包括量化器）、字符串操作和集合操作（包括通过uml关联和迭代器导航）以及let-in和if-then-else构造组成。表达式可以有标量类型（整数、布尔、字符串或uml类）或集合类型（包或集）。 这是ocl的一个重要部分，允许用户在uml模型上编写大多数有用的格式良好的约束，当新的ocl标准决定一些开放的问题并修复错误的问题（例如具有未知顺序的“有序集”）时，我们可能会在未来扩展它。关于动态部分，还定义了使用定义的静态部分的所有前置/后置条件构造，以及后置条件的特定构造K形式语义定义的主要优点是它们的可表达性、可执行性和模块性。每个ocl构造通常使用一个或两个K规则来定义。我们已经从K特性中受益匪浅，例如语法替换，用于评估严格操作的参数的K规则的自动生成，以及自动上下文转换器，这些功能只需要用户为匹配和重写提供具有最少信息的K个我们通过比较我们的let-inocl操作的K语义与附录A中的ocl标准的正式语义（信息性）来说明这些优点。我们还展示了符号OCL评价是如何获得的4独立于语言的匹配逻辑已经被定义[20]并正在实现。5.据我们所知，我们的方法是唯一处理符号评价的方法。A. Arusoaie et al. /Electronic Notes in Theoretical Computer Science 304（2014）8183∗∗以模块化的方式，仅仅通过用符号值扩展ocl数据类型，而不改变ocl的K语义规则中的任何内容。此外，我们开发的ocl实现符号求值的K模块也可以用于其他语言定义。本文的其余部分组成如下：第2节提供了一些关于uml，ocl和K框架的背景知识。在第3节中，我们给出了ocl的K定义，并举例说明。第4节总结并讨论了相关工作和今后的工作。一个实现我们定义的在线工具是可用的[1]。2背景2.1UML与OCL在本节中，我们回顾一些关于uml和ocl的概念。我们考虑uml类图的最小概念，包括：一组具有属性和方法声明的类（即，方法名与参数和返回值类型）;类之间的单向引用（或关联），其角色（或结束）具有[0.. ]多重性;类之间的推广偏序;和一组枚举。我们假设这些概念是已知的;更多信息可以在[17]中找到。类图的其他特性（双向引用，多重性不同于[0... ]、组合和聚合关联。. .）不被考虑，因为它们不添加任何表达性它们可以使用基本构造和OCL约束来等效地编码，如[10]中所示。我们要求属性有一个基本的类型（String ，Real ，Boolean ，String ，Enumeration），而关联只有对象集合类型。这就排除了属性是，例如，整数列表;然而，这不是限制，因为基本类型可以被包装在类中，并且属性可以被等效地转换为对那些类的引用。我们也排除了uml类图所允许的“有序”限定，因为它的语义是未指定的（它生成了具有未指定顺序的“有序集”UML对象图是类图的实例。它们由通过链接（关联的实例）连接的对象（类的实例，具有属性的值）组成。我们还假设这些概念是已知的。图1显示了一个类图和一个实例化它的对象图的例子。类图是为了模拟研究人员（其中一些是教授，另一些是博士生）撰写论文的情况，论文可能会提交给期刊。研究人员和期刊具有字符串值名称，而论文具有字符串值标题，布尔isSubmitted标记指示它们是否提交。Papers也有一个submit（）方法，它有一个空的参数列表和void返回类型。 前置和后置条件 在Paper类旁边的注释中编写教授有一个属性post：一个来自包含三个通常学术等级的Position枚举的值。博士生在一年的学习中，是一个（理论上，无界的）整数。也有几个协会（手稿，84A. Arusoaie et al. /Electronic Notes in Theoretical Computer Science 304（2014）81作者会场产品名称：字符串手稿context Pa-per：：submit（）：voidpre：isSubmitted= falsepost：isSubmitted= true+void submit（）name：Stringtitle：StringisSubmitted：Bool杂志研究员纸名称=“K'11”name=“Lucanu”post=fullProfessorentcs：日志多雷尔：教授title=“A K semantics forOCL”isSubmitted=b此：纸name=“Rusu”name=“Arusoaie”year=1vlad：研究员andrei：PhD Student博士生年份：教授职位：职位<<枚举>>位置副教授Fig. 1. 示例：类图（顶部）和对象图（底部）。Author，Venue），其中一些是双向的，并且是具有OCL约束的单向类的语法糖（如下所示）。图1底部的对象图是顶部类图的一个实例。注意，布尔属性isSubmitted有一个符号值，用变量b表示。也就是说，我们的对象图是符号化的，它表示通过类型一致的值实例化变量而获得的所有2.1.1OCL约束和限制OCL约束和查询是在UML类图上定义的，并在这些类图的UML对象图下面的约束可以在图1中的uml类图中定义：• 每篇论文至少有一位作者，最多链接到一个地点：Paper. allList（）→forAll（p |p.author →size（）≥ 1 × p.venue→size（）≤ 1）;• 如果提交了一份文件，那么它将被提交到一个地点：A. Arusoaie et al. /Electronic Notes in Theoretical Computer Science 304（2014）8185Paper. allList（）→forAll（p| p.isSubmitted隐含p.venue→size（）=1）;• 作者与手稿的关联形成双向关联。这意味着，对于每一篇论文，通过选取其每个作者，然后计算该作者Paper. allList（）→ forAll（p |p.author→ forAll（r|r.manuscript→includes（p）Researcher. allarr（）→ forAll（r |r.手稿→ forAll（p|p.author→includes（r））.w图1底部的对象图满足了这些约束。2.1.2方法的OCL前和后条件OCL还提供了用前/后条件注释方法的可能性。像往常一样，在调用方法之前，需要满足方法的前置条件，并且保证在方法完成时，其后置条件保持不变。前置条件可以是任何静态ocl约束，并且在方法被调用之前引用对象图的状态。后置条件也可以是任何静态ocl约束，并引用方法被调用后对象图的状态，除了由注释@pre前缀的类字段，它引用预状态。关键字return指的是方法的返回值（如果有的话）。方法submit（）的前置条件和后置条件分别是isSubmitted= false和isSubmitted = true。因此，在图1底部所示的符号模型上，应该不可能在this：Paper上调用submit（）两次。我们使用这个简单的例子来演示符号求值和前/后条件执行，并在第3节中展示如何在K中指定这些机制。2.2K框架K[22]是一个主要用于定义和分析编程语言语义的框架。K的主要特征包括：• 表现力：所有编程语言范例及其所有特定功能都以简单统一的方式描述• 模块化：每种语言特征都是一次性描述的，因此定义是可扩展的;• 可执行性：定义可直接执行，以便进行试验和分析;• 对程序推理的支持：该框架用作程序逻辑，利用该程序逻辑可以验证和分析程序（参见，例如，[20]）。语言的K定义具有以下主要成分：语法，其是语言的上下文无关的注释语法，并且从其提取计算任务;语言计算的值的定义;配置，其是抽象程序在其上执行的机器的状态结构的嵌套单元的结构;以及K规则，其描述程序在其上执行的状态。86A. Arusoaie et al. /Electronic Notes in Theoretical Computer Science 304（2014）81执行步骤使用最少的信息（仅匹配和重写所需的信息）。K工具[13]是K的当前原型，它将K定义作为输入，并使用几种复杂的算法将其转换为Maude [6]程序。然后，Maude程序可以用于自动执行和/或模型检查K定义[14]。3OCL的K定义在本节中，我们将通过以下步骤展示如何在K中定义ocl• 使用注释上下文无关语法定义ocl的语法• 定义OCL表达式可以计算的值;• 定义ocl的K配置;• 定义OCL语义的K规则。3.1语法我们对ocl的K定义的注释语法见附录A。我们目前支持常见的整数、实数和布尔表达式（包括带有量化器的布尔表达式）;字符串和串联;集合表达式，包括导航和迭代器;以及其他表达式（例如，let-in，if-then-else）。由于K定义是模的，我们可以添加新的表达式而不改变旧的表达式。请注意，ocl是一种不断发展的语言，K框架可以帮助实验语言中引入的新结构严格遵循某些产生式的注释指定了在计算定义的运算符之前必须计算哪些参数（详见[13]）。我们将看到这种机制是非常有用的，因为它将用户从书写中解放出来。用于评估构造的参数的K3.2OCL标准库ocl标准库[15]包括（见图2）：• 一组基本类型：Bool、String、Real和String;• 收集 类型，这 是 参数化在 的 T型：袋式T型，套装式T型，有序集T_n和序列T_n;• 一个超类型OclAny，任何uml类型或集合都是它的子类型;• 一个“最小”类型OclVoid，它是任何uml类型或集合的子OcIInvalid且具有唯一值null;• 一个“最小”类型OclInvalid，它是除OclVoid之外的任何uml类型和集合的子类型，并且具有唯一的值invalid。A. Arusoaie et al. /Electronic Notes in Theoretical Computer Science 304（2014）8187×→⟨ ⟩ ⟨ ⟩⟨ ⟩ ⟨ ⟩OclAny基元类型umltypes集合布尔雷亚尔序列编号TOrderedSet命令集设置T 袋式除尘器字符串OclVoid OclInvalid图二.OCL类型ocl原语类型是使用K内置类型（参见图3）Bool、Int、Float和String实现的。这些类型的值称为标量。我们还使用K内置的类型ID作为对枚举ocl类型的支持。我们已经扩展了所有带有符号值的ocl原语类型。在我们的设置中，符号值的形式为symBool（x）、symInt（x）、. . .，其中参数x是sortId。这种简单的机制使得符号模型上的ocl表达式的评估成为可能，而不改变ocl的K语义规则。这是因为K语义是模块化的，并且相同的定义可以在具有相同接口的各种数据域上执行。我们还定义了一个K模块，它用以下特定的数据类型扩展了上述内置类型：• Object作为所有uml类型的超类型。此类型的值是typedElt（o，C）对，其中o是对象引用，C是类名，因此o引用的对象是类型（C）的实例（=类C的类型）。• 一个类型Magma作为集合的超类型，例如，BagT和SetT。联合是一个由_ ;_表示的操作：Magma Magma Magma。对象是对象图中的元素，而集合是，在我们现在的定义，具有一个公共（超级）类型的标量列表。这意味着，在我们的运行示例中，允许教授和研究人员的集合，因为教授是研究人员的子类型，但不允许包含论文和期刊的集合，因为它们属于不同的类型。• 一个带有单例值null的Void类型，用于实现OclVoid。我们不实现OclInvalid类型。将invalid视为一个值会导致复杂化，因为它需要特定的规则来处理它。在我们的K定义中，invalid不是一个值：相反，它被定义为这样一个事实，即一个ocl表达式不会根据语义规则还原为一个值。因此，操作oclIsUndefined的实现是不必要的。在3.4节中给出了一个例子。我们不直接支持有序集合SequenceT和OrderedSetT。这些集合可以通过类图来建模，如图4所示。steoreotype_singleton_type表示类EmptySequence只有一个实例88A. Arusoaie et al. /Electronic Notes in Theoretical Computer Science 304（2014）811头：TNeSequence尾巴序列不⟨ ⟩⟨ ⟩OclAny对象收藏基元类型uml类型岩浆BoolBoolInt实数浮点数字符串套装T袋T袋OclVoidOclInvalidVoid图三.K实现的ocL类型。 K类型以颜色显示。<<单例>>空序列见图4。 序列图表示空序列。这实际上是一个更精确的建模，因为与有序集合不同，我们的图指定了一个顺序。如果需要，可以通过选择任意顺序，从包含有序集合的用户定义模型中自动生成此类图的实例。3.3配置ocl的K配置由五个主要单元组成• 一个包含计算任务序列的cell _ k;例如，它包括在计算ocl表达式时派生的计算任务。• 一个cell_metamodel，存储关于元模型的信息：名称、枚举类型和类。例如，第4页描述的类Paper由如下的单元结构表示：A. Arusoaie et al. /Electronic Notes in Theoretical Computer Science 304（2014）8189⟨ ⟩⟨ ⟩<类>
纸张/classname> . 联系我们 . 联系我们<方法><方法><方法名称>提交/方法名称><修改>已提交/修改> self.isSubmitted = true/post> self.isSubmitted = false/pre> void/return type><属性>isSubmitted|->bool title|-> string作者|->收藏<参考资料> . /references>注意，关联关系由属性（例如，作者）。• cell_constraints存储元模型的静态语义，表示为OCL约束列表。• 一个包含对象图的K表示的单元格模型，K单元格中的ocl类Paper的一个实例表示如下：<实例> paper/instName> Paper/ofClass><领域>已提交|-> typedElt（symbol（b），bool）标题|-> typedElt（“A K semantics for OCL”，string）authors|->typedElt（vlad，Researcher）;typedElt（dorel，Professor）;typedElt（andrei，PhDStudent）<联系我们其中属性isSubmitted具有符号值b。• 一个cell_output，它链接到标准输出，用于显示结果或错误消息。3.4语义在对象图上评估ocl表达式是根据ocl的语义来完成的，我们现在将其定义为一组K语义规则。我们从计算基本算术和布尔运算的简单规则开始。如下所示的分割规则如下：如果k单元格的顶部是一个除法表达式A/B，其中A和B的排序为Int，那么该表达式将被重写为使用K内建整数除法A/IntB，前提是规则A/BA/IntB···如果不是则返回（B=布尔0）90A. Arusoaie et al. /Electronic Notes in Theoretical Computer Science 304（2014）81因此，A/0形式的表达式不会被上述规则简化为一个合法的ocl值（这里是一个整数）。这样的表达式模拟了OCL标准的无效值[15]。我们的定义相对于标准的优点是，我们不需要给出明确的规则来说明无效值是如何传播的：包含未定义值的表达式（即，未归约为值的子表达式）也是unfined，因为它们未归约为值。大多数剩下的算术和布尔运算（附录A）都有类似的规则。下面我们展示了forAll量化器的规则;存在量化器的规则是通过对偶获得的。forAll的K语义规则是：（·）→forAll（Var|Exp）true···中国（1）（Elt，Rest）→for All（Var |Exp）如果Exp[Elt/Var]，则Rest→forAll（Var|Exp）else false···中国（2）第一个规则描述了基本情况，当第一个参数是空集合时。第二条规则描述了归纳步骤：当第一个参数是一个非空的集合，形式为（Elt，Rest），结果取决于表达式Exp在元素Elt上的值。这是通过将K库如果该值为true，则总体结果是forAll操作的结果，在集合Rest上递归计算;否则，结果为false。这个相对简单的定义是可能的，因为有几种强大的机制，K. 其中之一是替换操作符，它实际上是在K本身中使用访问者模式实现的[22]。我们将在本节后面的定义let-in表达式的语义并将其与ocl标准中相应的语义进行比较时回到替换运算符[15]。我们在这里广泛使用的另一个K机制是自动生成计算严格运算符参数的规则记住（cf.附录A），forAll在其第一个参数中是严格的这意味着在计算forAll为了做到这一点，K自动生成以下形式的规则：E1→forAll（V|E2）E1aQ→forAll（V|E2）第一个计算任务变成了对表达式E1的求值;“根据E1的结构，这可以使用相同的机制生成更多的任务。A. Arusoaie et al. /Electronic Notes in Theoretical Computer Science 304（2014）8191⟨ ⟩⟨ ⟩⟨ ⟩当E1被计算为一个真集合时，比如说，L，K规则的形式L a Q→forAll（V|E2）L → for All（V|E2）填补E1留下的最后，其中一条规则（1现在让我们来谈谈集合的规则。选择和收集操作与规则（1- 2）非常相似相反，我们展示了K规则，它为查询alllog（）提供了语义：中文（简体）collectAllInstanceNames（Cls，children（Cls，M），M）···该规则表明，为了计算对象图M中给定类Cls的实例，调用一个辅助函数collectAllInstanceNames（），其中包含三个参数：类Cls、其子类Cls和M本身。K规则可以在不同的配置单元格中进行多次局部重写，并且可以使用其他单元格为重写提供上下文。例如，在上面的规则中，cell_model提供了图M。函数children（）通过遍历M来计算给定类的子类，collectAllInstanceNames（）遍历M的实例单元格，收集它们的名称，并将它们放在一个包中返回。另一个集合表达式，其语义广泛使用_instance单元格是导航操作。它的语义规则是：（·）。澳大利亚铁路研究所········（Elt，Rest）。属性值联合（剩余）attr）···第一个规则是基本情况：它通过一个空集合的属性attr计算导航;结果是空的。第二个规则是归纳步骤。对于非空集合（Elt，Rest），结果是AttrValue与递归地将操作应用于集合Rest的结果之间的联合。在这里，AttrValue是attr属性的值，它来自于_注意，只给出了从单元格所需的最小信息：例如，我们只给出了部分匹配for_instance单元格，而不必说任何关于配置的周围单元格的事情。该信息由K上下文Transformer机制自动合成[22]。现在我们转向let-in操作，并比较它的K语义与92A. Arusoaie et al. /Electronic Notes in Theoretical Computer Science 304（2014）81¢{<$）}{<$） }）K标准的语义[15]。 K语义很简单：小峰Var=实验中的Val实验[Val/Var]···中国（3）也就是说，let-in操作只是Ksubstitution_[_/_]的语法糖。当前标准[15]（第209页）中let-in的语义如下：I<$令v=e1ine2）（r） =I<$e2）（σ，β{v/e1）（r）}）左边是我让v=e1在e2（r）中的解释设在环境r中v=e1，e2。 后者是一对（σ，β），模型σ，其中执行评估，以及环境β- a函数将e1，e2中的自由变量映射到值。右边是环境（σ，β v/ e1（r））中e2的解释，其中β v/ e1（r）是r的β分量，修改为使得v与e1的解释绑定。注意由（σ，β）对和由e1的解释引入的额外复杂性。在我们的例子中，我们不需要指定模型σ，因为K上下文转换会自动推断它，我们也不需要使用显式的变量环境β，因为内置的K语法替换会用变量的值替换变量。此外，我们不需要参考e1的解释，因为第二个参数中let-in结构的严格性注释确保了这个参数是一个值-在（3）中由Val表示-当let-in被求值时。最后，我们将展示如何处理方法调用，并在一个示例中说明它们。为了简单起见，我们只展示了没有参数的方法的情况我的天M（）evaluate（Pre）aupdate（O，C，F）aevaluate（Post）·············该规则包括评估前置条件，更新模型，并评估后置条件。请注意，evaluate结构是严格的：当调用以下规则时，其参数已经被评估为（可能是符号）布尔值评估（B）····BJ和布尔B约束条件还有更新模型的规则，由于空间不足，这里没有显示下面的简单示例说明了方法调用和符号计算的使用。该示例包括在this：Paper对象上调用两次submit方法（参见 图1）。 预期的结果是，不可行。第一次调用后，约束单元格的内容为：symBool（b）= false和Bool symBool（var0）= trueA. Arusoaie et al. /Electronic Notes in Theoretical Computer Science 304（2014）8193其中第一个相等是前提条件，第二个是后置条件;这里，symBool（var 0）是由模型更新规则分配给属性isSubmitted的符号值。在第二次调用之后，单元格的内容变为symbBool（b）= false和Bool symbBool（var0）= true和BoolsymbBool（var0）=false和Bool symbBool（var1）=true由于条件的计算结果为false，因此方法调用序列是不可行的。我们已在Maude就该等条件实施满意度检查程序，处理最常见的情况。对于更复杂的情况，可以通过调用专门的约束求解器来检查满足性。我们得到以下输出：$ krun测试不可行;约束简化为false。4结论、相关工作和未来工作对象约束语言的最初设计目标是为UML提供一种清晰、易于理解和正式的规范语言，以补充不太正式的图。不幸的是，当前标准中语言的实现缺乏最初设想的许多质量。在本文中，我们集中在更好地理解部分的ocl，并提供了一个正式的语义在K框架。在简单性方面我们的语义与ocl标准[15]的信息附录中相应的数学/形式定义相我们的方法的一个显着特点是符号评估的ocl表达式，我们 通 过 一 个 例 子 说 明 ， 一 个 序 列 的 方 法 调 用 是 不 可 行 的 ， 由 于insatisfiableocl约束产生的方法的前，后条件。我们已经实现了一个从文本格式的类图、对象图和ocl表达式到K代码的翻译器然后将代码与Kocl语义一起编译最终的工具可在线获取[1]。ocl的定义在不断发展，我们相信使用语言标准的K将大大提高未来版本的质量。相关工作我们已经提到了ocl标准的资料性附录[15]。尽管主要由于许多错别字而存在缺陷，但附件是基于坚实的正式地面集理论基础[19]。我们不知道有什么正式的工具可以实现ocl标准的集合论语义最接近我们的方法是基于Maude重写系统的几个方法：[21]根据作者的说法，它实现了完整的OCL标准;[3]在元建模框架中使用OCL;[7]还实现了过程，这使得OCL非常接近编程语言。作者使用了在形式化他们的ocl语义时获得的经验来构建一个用传统编程语言编写的ocl评估器的有效实现[8]。另一个接近实现完整标准的学术工具，也是用传统的编程语言编写的，但不是基于94A. Arusoaie et al. /Electronic Notes in Theoretical Computer Science 304（2014）81在一个正式的语义上，是OCL评估器[5]。ocl的各种其他实现存在于模型转换语言中，例如qvt标准[16]，atl[11]和KerMeta[18]语言。ocl语义也在交互式定理证明器中定义：[2]在KeY中，[12]在PVS中，[4]在Isabelle/HOL中。这些工具需要人的交互来评估ocl约束，不像我们的和上面提到的所有工具。我们目前对这些工作的主要贡献是ocl表达式的符号求值，据我们所知，这在这个框架中是新的。未来的工作这是我们正在进行的研究项目的一部分，该项目旨在为特定领域的建模语言定义基于K的操作语义[23]。ocl表达式的符号评估将用于检查场景的可行性和执行形式验证。从更实际的角度来看，我们正在计划实现用于对“真正的”uml模型进行去糖的工具组合和聚合操作，并使用有序集合类型）到约束模型的最小我们的目标是使我们的工作可供外部用户使用。确认作者感谢匿名评论者提出的宝贵和建设性的意见和建议。本文中提出的研究得到了DAK项目合同161/15.06.2010，SMIS-CSNR 602-12516的部分支持。引用[1] ***，MLK- 在线工具（2011年）。网址https://fmse.info.uaic.ro/tools/mlk/[2] Beckert，B.，联合Keller和P. H. Schmitt，将对象约束语言转换为一阶谓词逻辑，在：会议记录，验证，联邦逻辑会议研讨会（FLoC），哥本哈根，丹麦，2002年，交互式/演绎验证。[3] Boronat，A.和j.Meseguer，OCL约束元模型规范的代数语义学，在：TOOLS（47），Lecture Notes in Business Information Processing33（2009），pp.96比115[4] Brucker，A. D.和B.吴文龙，UML/OCL的形式化证明环境，见：J.L. Fiadeiro和P.Inverardi，editors，FASE，Lecture Notes in Computer Science4961（2008），pp.97比100[5] Chiorean，D.，M. Pasca，A.克尔库角Botiza和S. 使用OCL环境性。注意Theor。Comput. Sci. 102（2004），pp.99[6] Clavel，M.，F. Duran，S. Eker，P. Lincoln，N. Martí-Oliet，J. Meseguer和C. L.塔尔科特“ All AboutMaude, A High-Performance Logical Framework,” Lecture Notes in Computer Science[7] Clavel ， M. 和 M. Egea ， ITP/OCL ： A Rewriting-Based Validation Tool for UML+OCL Static ClassDiagrams，in：AMAST，Lecture Notes in Computer Science4019（2006），pp.368-373.[8] Clavel，M.，M. Egea和M. A. G. de Dios，Building an Efficient Component for OCL Evaluation，ECEASST15（2008），Maude OCL语义的更有效实现[9] 埃 里 森 角 和 G. Roanzu ， C与 应 用 程 序 的 可 执 行 形 式 语 义 ， 在 ： 第 39届 编 程 语 言 原 理 研 讨 会 论 文 集（POPL533-544.A. Arusoaie et al. /Electronic Notes in Theoretical Computer Science 304（2014）8195[10] Gogolla，M.和M. Richters ，用于 UML类图的变换规则，在：J. Bézivin 和P.-A. Muller，editors ，UML，Lecture Notes in Computer Science1618（1998），pp.92比106[11] Jouault，F.，F. Allilaire，J. Bézivin and I. Kurtev，ATL：一个模型转换工具，Sci。Comput.程序. 72（2008），pp. 31比39[12] Kyas，M.，H. Fecher，F. S. de Boer，J. Jacob，J. Hooman，M. van der Zwaag，T. Arons和H. Kugler，在PVS中形式化UML模型和OCL约束，电子笔记理论。Comput. Sci. 115（2005），pp. 39比47[13] Lazar，D.，A. Arusoaie，T. F.塞尔巴努塔角埃里森河梅勒乌塔湾Lucanu和G. Roanzu，用K工具执行形式语义，在：第18届形式方法国际研讨会论文集（FM[14] Lucanu，D.，T. F. nuanjiang和G. Rou，K框架蒸馏，在：第九届重写逻辑及其应用国际研讨会，2012年，第9页，邀请谈话。[15] 对象管理组，对象约束语言，版本2.2，技术报告（2010），http://www.omg.org/spec/OCL/2.2/。[16] 对象管理组，Meta Object Facility（MOF）2.0 Query/View/ Transformation Specification，技术报告（2011），http://www.omg.org/spec/QVT/1.1/PDF/。[17] Objet管理小组，统一建模语言，技术报告，http://www.uml.org/。[18] Muller ， P. 一 、 F. Fleurey 和 J. -M. Jézéquel ， Weaving Executability into Object-Oriented Meta-languages，in：MoDELS，Lecture Notes in Computer Science3713（2005），pp.264-278。[19] Richters，M.，“OCL约束”，博士论文，Universität Bremen（2002），使用集合论形式化OCL，它构成了标准的信息性附录的基础[20] Rozelu，G.，C. Ellison和W.Schulte，匹配逻辑：Hoare/Floyd逻辑的替代方案，在：M. Johnson和D. Pavlovic，editors，Proceedings of the 13th International Conference on AlgestheticMethodology And Software Technology（AMAST142比162[21] Roldán，M.和F. Durán，Dynamic Validation of OCL Constraints with mOdCL，ECEASST44（2011），maude implementation of OCL invariant，pre，and post condition evaluation.[22] 罗 乌 湾 和 T.- F. K Semantic Framework 的 概 述 ， Journal of Logic and Algebras Programming79（2010），pp. 397-434.[23] Rusu，V.和D. Lucanu，A K-Based Formal Framework for Domain-Specific Modeling Languages，第二届 面 向 对 象 软 件 形 式 化 验 证 国 际 会 议 ， 2011 年 ， 第 10 页 。 306 网 址 http://foveoos2011.cost-ic0701.org/A邻氯苯酚钾当前版本的ocl的K定义只包含OMG标准的内核。由于K的模块性，新的指令可以在不改变现有指令语义的情况下增量添加。A.1算术表达式合
