基于Object-Z生成Python代码的研究

袁鼎 刘振宇

摘要    在本文中，我们将提出一种从OZ到Python的映射去验证这些规范。在这个映射中，包括前置条件、后置条件和变量都将被验证，这些都是建立在使用lambda函数（以下简称L函数）和Python的编辑器上的。本研究发现Python对于开发从OZ映射到Python的函数库来说是一种相对完美的语言。

【关键词】Object-Z Python 面向对象编程 契约式设计

1 概述及相关工作

形式化语言0Z是基于面向对象编程的，相对于其他形式化语言，OZ语言有更加重要的特征，具体如下：

（1）强有力的语义和运算（谓词运算和集合论）。

（2）强大的对象支持。

（3）其规范类型直接和面向对象编程构造相对应。

然而，通过形式化语言来进行形式化证明是一项很困难的任务，它需要许多数学技巧，并且要找到一种能够把0Z语言映射到编程语言，并且在执行期间能够验证这种规范的方法。许多研究人员已经做了许多关于映射0Z到面向对象编程语言的工作，比如C++和Java等等。这其中有些研究表示的是一种映射方法，它包含了一些0Z结构如基本类型、模式、类、状态模式、操作运算符、状态模式谓词等等。

此外，有些研究人员还做了关于映射0Z到包含合并规范概念的面向对象规范语言方面的研究。这些对应链接可以允许系统需求在高级形式化语言中被明确规定，并且可以在编程层面进行验证。

不同于0Z映射中的C++等编程，Python支持多元模式、动态分类、高级嵌入式数据类型、许多可利用的扩展了数据计算能力的扩展包。它集合了谓词运算、集合论、定理证明去验证这些文字性的规范。这使得它非常适合用在科学化和形式化规范映射当中，本文实现了映射一部分0Z规范到Python编程层面的规范。

2 研究背景

我们先回顾一下0Z的主要结构，我们选择Python编程去映射0Z的原因，然后考虑通过契约式设计去验证从0Z映射到Python的协议。

2.1 OZ

OZ是Z语言的扩充，它在此基础上增加了面向对象的模式构建，比如类和其他面向对象的概念（并发性、单1多继承等）。Z语言是基于数学符號比如集合论，L函数和一阶谓词逻辑，Z语言表达式是使用数学函数和谓词来进行分类的。

在OZ中，类定义由一个已命名的伴随可选择形式化参数的“盒子”所构成。这个“盒子”介绍一个基本类型仅仅使用了一个表达式或者谓词，或者可能拥有一个可见性列表、可继承的类、本地类型和常量定义。

我们尝试以一个OZ规范为范例，它描述.了一个简易的信用卡银行账户系统。每个账户有两个数据（当前余额和信用额度）和两个操作（取出、存入）。该0Z规范范例将在接下来的章节中被一步步转化为执行代码。

2.2 Python

Python是一种强大的编程语言，它支持多个范例、动态分类、自动存储器管理、高层的内置数据类型、分层的包和许多可供选择的附加包。这些包扩展了它的数据计算、科学化图形和图形化用户界面编程等方面的能力，这些使它在科学编程中变得非常有用。

它和OZ语言有许多相似性。他们都是基于面向对象模式，包含了谓词运算和集合论。因此，它是一种自然而然更加接近形式化规范的功能性编程语言。

它有非常简单的语法，阅读它的程序就像是阅读英文一样。用它写的程序仅仅只有用C++等语言编程的代码量的一半左右。它集中于问题的解决办法而不是语言本身，因为它的开源特征，如果你避开了所有的系统相关特征，它的代码可以被应用于许多平台而不需要任何改变。

Python和0Z语言有许多相似性。它们都是基于面向对象模式，包含了谓词运算和集合论。因此，它是一种自然而然更加接近形式化规范的功能性编程语言。

2.3 契约式设计

契约式设计是一.种过去常用来控制两个模块间的交互的软件验证性方法，它通过基于前置条件和后置条件准则的精确规范来确保编程和规范之间的-致性。对于Python编程来说，已经有许多契约式设计包比如PyContract等允许注释契约表达式的功能，但是这些包使用了一种不允许扩充契约表达式的语法，它不能表示不变量到类属性，这些契约也仅仅只能处理本地范围内的函数变量。

功能契约由前置条件和后置条件组成，在本文中，前置条件修饰符“pre”表示执行一个函数之前应该满足的条件。同理，后置条件修饰符“post”表示在执行完该函数后必须要达到的目标。这些“pre”和“post”修饰符也可以应用于类方法，上。此外，不变量修饰符“inv”表示类实例无论在调用前还是调用后总是返回真。“pre”“post”“inv”修饰符以L函数作为参数来验证类或者方法上的约束。

3 OZ到Python的映射

3.1 类定义

OZ中的类模式可以通过封装本地类型、常量声明、初始化状态模式、零或更多给定状态的操作模式来引进类的概念。

规则1：每一个OZ类模式等同于一个同名的Python类声明，不考虑任何形式的通用参数类型是否退出，因为Python是一种在运行时验证信息类型安全的动态类型检查语言。

3.2 可见性列表

在OZ可见性列表中，所有发现的成员对于类对象的环境来说都是可见的。在可见性列表中未被发现的成员仅对类的对象及其所有派生类可见。默认情况下，Python中的所有类成

员都是共有的，如果它的名字有两个强调不能被外部类访问的前缀就表明它是私有的。

规则2：一个未在可见性列表中发现的类的所有成员将通过其名称预先用两个下划线预编译为私有。这些下划线将可以通过它的名称在同一个类中被访问，或者通过它的父类名称在派生类中被访问，否则默认为是公有的。

3.3 常量声明

在OZ中，常量声明与类相关，它有固定值并且不被类的任何操作所改变，但它在有些类中可能有不同。因为编写函数比编写类更加容易，而Python對象可以充当函数对象，所以我们可以将这些类型声明映射到由类型条件验证修饰的函数上。

规则3：每个常量声明都将被映射到一个由“pre”谓词修饰的函数，用来检验常量类型及其初始化。

3.4 常量模式谓词

常量模式谓词是指在模式中为常量提供正确值的谓词。

规则4：常量模式谓词将被映射到使用L函数来检查常量正确值的“inv”修饰器。

3.5 状态模式

状态模式是表示一个声明属性值对应于类变量的构造，并通过谓词来确定它们值之间的正确关系。

规则5：在状态模式中，每-一个变量都将被映射到类属性上，它的状态谓词将被视为一个不变的类修饰器“inv”。

主变量要么是可见的，要么是不可见的。不可见的变量（属性）需要从两个下划线符号开始，因此它不能被外部类修改。如果变量和不变量相关联以确保它的正确性，则该模式必须拥有检查属性值的不变量。

3.6 初始状态模式

初始状态模式没有声明部分，它的谓词限制了状态变量和类常量的可能值。初始模式决定了所有已创建对象的初始状态，并始终命名为init。

规则6：初始状态模式将映射到制定了所有已创建对象初始值的_init_构造函数。

3.7 操作模式

规则7：每个操作模式都将映射到一个Python方法及其相关的输入声明，其谓词列表将映射到L前提条件和后置条件的集合。

3.8 对象交互

我们以两个信用卡为类实例，描述存款，以及不用卡之间的取款及资金转移等基本功能。

3.8.1 辅助变量

辅助变量可能根据类中出现的主变量而发生变化，因此主变量的任何更改都会影响辅助变量，更改主变量的操作必须更新辅助变量。

规则8：编写一个函数来更新辅助变量，以防主变量值发生改变，并且用此函数来修饰类。在调用类中的任何方法以根据与这些变量相关的不变状态更改辅助变量之后，将调用此更新函数。

在我们的函数库中找到了修饰所有函数实现，用于在调用更改辅助变量的类中的任何方法之后调用大括号之间出现的函数。

3.8.2 初始模式引用

object._init_（self）是对“object”的初始模式的调用。

3.8.3 非确定性选择

非确定性选择运算符用于对一对运算中的至多一个运算的出现进行建模，并且当两个运算都被启用时，将非确定性地选择运算。

3.8.4 顺序组合

顺序组合运算符等效于执行第一个运算，然后执行第二个运算，第一个运算输出变量被识别并与具有相同基本名称的第二个运算的输入变量等同，这意味顺序组合等效于并行组合。映射如下：

OpExp3：=OpExp1;OpExp2

3.8.5 并行组合

并行识别运算符II用作模式管道运算符，它通过在一个操作中识别和等同输入变量与具有相同名称的其它操作中的输出变量来结合操作表达式。并行组合运算操作符可以表示如下：

OpExp3：=OpExp1IIOpExp2

规则9：以上形式的并行运算符可以被映射成：

op3=parallel（opl，op2）

where

defparallel（shl，sh2，*kwargs）：

returmlambda*kwargs：sh2（shl（*kwargs））**kwargs是一个字典，它结合了两种模式的输入，每个输入都可以通过字典访问，例如访问x的值，我们写成kwargs[x]。

这对所有的并行运算都有效，如果在第一个模式的输出和第二个模式的输入中存在具有相同名称和类型的变量，则第一个模式调用参数传递给第二个模式，该参数被视为通过引用调用。

4 总结与展望

编程语言具有不同的风格和范例，具有不同的优点和缺点。在将C++和Java编程映射到0Z方面已经做了许多的努力，但是流行度和面相对象编程范例更加倾向于本文中这种映射。Python是一种多范式编程语言，动态类型、高级内置数据类型和许多附加软件包，它包含谓词演算、数学证明、集合论和许多库。除此之外，它还可以扩展包含新的符号和特征。

Python和OZ语言有许多相似之处。它们都是基于面向对象的范式.集合论和谓词演算，而且Python是一种函数式编程语言，它自然更接近形式化规范。

本工作发现Python是一种很好的语言，用于开发库来映射0Z规范，这些规范使用Python的修饰功能来扩展具有前提条件、后置条件和不变式符号的语言以检查功能约束。此外，通过编写这些符号使其成为可能通过几个简单的步骤将规范转换为实现。实际上，这些符号将通过执行它们而不是执行证明来验证。未来的工作可以完成此处未涉及的所有其它OZ构造，并可以将OZ形式规范转换为自动化实现。

参考文献

[1]汤小康.基于UML和Z的需求分析到软件体系结构的映射研究[D].湖南师范大学，2007.

[2]燕昊.UML建模的形式化研究[D].兰州大学，2006.

[3]周瑾，马应龙，李巍等.UML的形式化及其应用[J].计算机科学，2005，32（03）：136-140.

[4]文志诚，缪淮扣，张新林。基于0bject-Z的形式化验证方法[J].计算机科学，2007，34（05）：247-251.

[5]解方.从UML建模到Z形式化规范的研究[D].太原理工大学，2013.

[6]汤小康，王志刚，曹步文.UML用例图的Z形式规范[J].计算机与现代化，2006（11）：12-13.