您现在的位置是：首页 > 技术资料 > 基于Object-Z生成Python代码的研究

推荐星级：

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

更新时间：2019-12-20 23:11:13 大小：1M 上传用户：songhuahua 查看TA发布的资源 标签：object python 下载积分：1分评价赚积分（如何评价?）打赏收藏评论(0) 举报

资料介绍

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

部分文件列表

文件名	大小
基于Object-Z生成Python代码的研究.pdf	1M

立即下载

【关注B站账户领20积分】

部分页面预览

（完整内容请下载后查看）

程序设计

Program Design

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

文/袁鼎刘振宇

在科学化和形式化规范映射当中，本文实现了

映射一部分OZ 规范到Python 编程层面的规

范。

它的代码可以被应用于许多平台而不需要任何

改变。

在本文中，我们将提出一

种从OZ到Python的映射去验证

这些规范。在这个映射中，包括

前置条件、后置条件和变量都

将被验证，这些都是建立在使用

lambda函数(以下简称L函数)

和Python的编辑器上的。本研究

发现Python对于开发从OZ映射

到Python的函数库来说是一种相

对完美的语言。

摘

要

Python 和OZ 语言有许多相似性。它们都

是基于面向对象模式，包含了谓词运算和集合

论。因此，它是一种自然而然更加接近形式化

规范的功能性编程语言。

2 研究背景

我们先回顾一下OZ 的主要结构，我们

选择Python 编程去映射OZ 的原因，然后考

虑通过契约式设计去验证从OZ 映射到Python

的协议。

2.3 契约式设计

契约式设计是一种过去常用来控制两个

模块间的交互的软件验证性方法，它通过基于

前置条件和后置条件准则的精确规范来确保编

程和规范之间的一致性。对于Python编程来说，

已经有许多契约式设计包比如PyContract 等允

许注释契约表达式的功能，但是这些包使用了

一种不允许扩充契约表达式的语法，它不能表

示不变量到类属性，这些契约也仅仅只能处理

本地范围内的函数变量。

2.1 OZ

【关键词】Object-Z Python 面向对象编程

OZ 是Z 语言的扩充，它在此基础上增加

了面向对象的模式构建，比如类和其他面向对

象的概念（并发性、单/ 多继承等）。Z 语言

是基于数学符号比如集合论，L 函数和一阶谓

词逻辑，Z 语言表达式是使用数学函数和谓词

来进行分类的。

契约式设计

1 概述及相关工作

形式化语言OZ 是基于面向对象编程的，

相对于其他形式化语言，OZ 语言有更加重要

的特征，具体如下：

功能契约由前置条件和后置条件组成，

在本文中，前置条件修饰符“pre”表示执行

一个函数之前应该满足的条件。同理，后置条

件修饰符“post”表示在执行完该函数后必须

要达到的目标。这些“pre”和“post”修饰符

也可以应用于类方法上。此外，不变量修饰符

“inv”表示类实例无论在调用前还是调用后

总是返回真。“pre”“post”“inv”修饰符

以L 函数作为参数来验证类或者方法上的约

束。

在OZ 中，类定义由一个已命名的伴随可

选择形式化参数的“盒子”所构成。这个“盒

子”介绍一个基本类型仅仅使用了一个表达式

或者谓词，或者可能拥有一个可见性列表、可

继承的类、本地类型和常量定义。

（1）强有力的语义和运算（谓词运算和

集合论）。

（2）强大的对象支持。

我们尝试以一个OZ 规范为范例，它描述

了一个简易的信用卡银行账户系统。每个账户

有两个数据（当前余额和信用额度）和两个操

作（取出、存入）。该OZ 规范范例将在接下

来的章节中被一步步转化为执行代码。

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

造相对应。

然而，通过形式化语言来进行形式化证

明是一项很困难的任务，它需要许多数学技巧，

并且要找到一种能够把OZ 语言映射到编程语

言，并且在执行期间能够验证这种规范的方法。 2.2 Python

3 OZ到Python的映射

许多研究人员已经做了许多关于映射OZ 到面

Python 是一种强大的编程语言，它支持

向对象编程语言的工作，比如C++和Java等等。

这其中有些研究表示的是一种映射方法，它包

含了一些OZ 结构如基本类型、模式、类、状

态模式、操作运算符、状态模式谓词等等。

此外，有些研究人员还做了关于映射OZ

到包含合并规范概念的面向对象规范语言方面

的研究。这些对应链接可以允许系统需求在高

级形式化语言中被明确规定，并且可以在编程

层面进行验证。

3.1 类定义

多个范例、动态分类、自动存储器管理、高层

的内置数据类型、分层的包和许多可供选择的

附加包。这些包扩展了它的数据计算、科学化

图形和图形化用户界面编程等方面的能力，这

些使它在科学编程中变得非常有用。

OZ 中的类模式可以通过封装本地类型、

常量声明、初始化状态模式、零或更多给定状

态的操作模式来引进类的概念。

规则1：每一个OZ 类模式等同于一个同

名的Python 类声明，不考虑任何形式的通用

参数类型是否退出，因为Python 是一种在运

行时验证信息类型安全的动态类型检查语言。

它和OZ 语言有许多相似性。他们都是基

于面向对象模式，包含了谓词运算和集合论。

因此，它是一种自然而然更加接近形式化规范

的功能性编程语言。

不同于OZ 映射中的C++ 等编程，Python

支持多元模式、动态分类、高级嵌入式数据类

型、许多可利用的扩展了数据计算能力的扩展

包。它集合了谓词运算、集合论、定理证明去

验证这些文字性的规范。这使得它非常适合用

3.2 可见性列表

它有非常简单的语法，阅读它的程序就

像是阅读英文一样。用它写的程序仅仅只有用

C++ 等语言编程的代码量的一半左右。它集中

于问题的解决办法而不是语言本身，因为它的

在OZ 可见性列表中，所有发现的成员对

于类对象的环境来说都是可见的。在可见性列

表中未被发现的成员仅对类的对象及其所有派

开源特征，如果你避开了所有的系统相关特征，生类可见。默认情况下，Python 中的所有类成

●项目基金：（基金编号：2018KYY086）本研究受南华大学研究生科研基金支持。

电子技术与软件工程ꢀꢀ

Electronic Technology & Software Engineering

234 ·

Program Design

程序设计

员都是共有的，如果它的名字有两个强调不能

被外部类访问的前缀就表明它是私有的。

规则2：一个未在可见性列表中发现的类

的所有成员将通过其名称预先用两个下划线预

编译为私有。这些下划线将可以通过它的名称

在同一个类中被访问，或者通过它的父类名称

在派生类中被访问，否则默认为是公有的。

3.8 对象交互

我们以两个信用卡为类实例，描述存款，

用调用。

4 总结与展望

以及不用卡之间的取款及资金转移等基本功

能。

编程语言具有不同的风格和范例，具有

不同的优点和缺点。在将C++ 和Java 编程映

射到OZ 方面已经做了许多的努力，但是流行

度和面相对象编程范例更加倾向于本文中这种

映射。Python 是一种多范式编程语言，动态类

型、高级内置数据类型和许多附加软件包，它

包含谓词演算、数学证明、集合论和许多库。

除此之外，它还可以扩展包含新的符号和特征。

Python 和OZ 语言有许多相似之处。它们

都是基于面向对象的范式、集合论和谓词演算，

而且Python 是一种函数式编程语言，它自然

更接近形式化规范。

3.8.1 辅助变量

辅助变量可能根据类中出现的主变量而

发生变化，因此主变量的任何更改都会影响辅

助变量，更改主变量的操作必须更新辅助变量。

规则8：编写一个函数来更新辅助变量，

以防主变量值发生改变，并且用此函数来修饰

类。在调用类中的任何方法以根据与这些变量

相关的不变状态更改辅助变量之后，将调用此

更新函数。

3.3 常量声明

在OZ 中，常量声明与类相关，它有固定

值并且不被类的任何操作所改变，但它在有些

类中可能有不同。因为编写函数比编写类更加

容易，而Python 对象可以充当函数对象，所

以我们可以将这些类型声明映射到由类型条件

验证修饰的函数上。

在我们的函数库中找到了修饰所有函数

实现，用于在调用更改辅助变量的类中的任何

方法之后调用大括号之间出现的函数。

3.8.2 初始模式引用

规则3：每个常量声明都将被映射到一个

由“pre”谓词修饰的函数，用来检验常量类

型及其初始化。

本工作发现Python 是一种很好的语言，

用于开发库来映射OZ 规范，这些规范使用

Python 的修饰功能来扩展具有前提条件、后置

条件和不变式符号的语言以检查功能约束。此

外，通过编写这些符号使其成为可能通过几个

简单的步骤将规范转换为实现。实际上，这些

符号将通过执行它们而不是执行证明来验证。

未来的工作可以完成此处未涉及的所有其它

OZ 构造，并可以将OZ 形式规范转换为自动

化实现。

object.__init__(self) 是对“object”的初始

模式的调用。

3.4 常量模式谓词

3.8.3 非确定性选择

常量模式谓词是指在模式中为常量提供

正确值的谓词。

非确定性选择运算符用于对一对运算中

的至多一个运算的出现进行建模，并且当两个

运算都被启用时，将非确定性地选择运算。

3.8.4 顺序组合

规则4：常量模式谓词将被映射到使用L

函数来检查常量正确值的“inv”修饰器。

3.5 状态模式

顺序组合运算符等效于执行第一个运算，

然后执行第二个运算，第一个运算输出变量被

识别并与具有相同基本名称的第二个运算的输

入变量等同，这意味顺序组合等效于并行组合。

映射如下：

状态模式是表示一个声明属性值对应于

类变量的构造，并通过谓词来确定它们值之间

的正确关系。

参考文献

[1]汤小康. 基于UML和Z的需求分析到软

件体系结构的映射研究[D].湖南师范大

学,2007.

规则5：在状态模式中，每一个变量都将

被映射到类属性上，它的状态谓词将被视为一

个不变的类修饰器“inv”。

OpExp3 ::= OpExp1 ; OpExp2

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

学,2006.

3.8.5 并行组合

并行识别运算符|| 用作模式管道运算符，

它通过在一个操作中识别和等同输入变量与具

有相同名称的其它操作中的输出变量来结合操

作表达式。并行组合运算操作符可以表示如下：

OpExp3 ::= OpExp1 || OpExp2

[3]周瑾,马应龙,李巍等.UML的形式化及其

应用[J].计算机科学,2005,32(03):136-

140.

主变量要么是可见的，要么是不可见的。

不可见的变量（属性）需要从两个下划线符号

开始，因此它不能被外部类修改。如果变量和

不变量相关联以确保它的正确性，则该模式必

须拥有检查属性值的不变量。

[4]文志诚,缪淮扣,张新林.基于Object-Z

的形式化验证方法 [J]. 计算机科

学,2007,34(05):247-251.

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

射成：

3.6 初始状态模式

[5]解方.从UML建模到Z形式化规范的研究

[D].太原理工大学,2013.

op3 = parallel(op1, op2)

初始状态模式没有声明部分，它的谓词

限制了状态变量和类常量的可能值。初始模式

决定了所有已创建对象的初始状态，并始终命

名为init。

where

[6] 汤小康 , 王志刚 , 曹步文 .UML 用例

图的 Z 形式规范 [J]. 计算机与现代

化,2006(11):12-13.

def parallel(sh1, sh2, *kwargs):

return lambda *kwargs: sh2(sh1(*kwargs))

**kwargs 是一个字典，它结合了两种模

式的输入，每个输入都可以通过字典访问，例

如访问x 的值，我们写成kwargs[x]。

这对所有的并行运算都有效，如果在第

一个模式的输出和第二个模式的输入中存在具

有相同名称和类型的变量，则第一个模式调用

参数传递给第二个模式，该参数被视为通过引

规则6：初始状态模式将映射到制定了所

有已创建对象初始值的__init__ 构造函数。

作者简介

袁鼎（1994-），男，硕士研究生，主要从事

3.7 操作模式

UML的形式化方面的研究。

规则7：每个操作模式都将映射到一个

Python 方法及其相关的输入声明，其谓词列表

将映射到L 前提条件和后置条件的集合。

作者单位

南华大学计算机学院湖南省衡阳市 421001

电子技术与软件工程

Electronic Technology & Software Engineering

· 235

全部评论(0)

暂无评论

评论赚积分>>

上传资源上传优质资源有赏金

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

资料介绍

部分文件列表

部分页面预览

相关下载

全部评论(0)

热门标签

最新上传

热门下载

资料专题

推荐下载

专栏首页