基于契约式设计的VeriJava编程语言设计

2014-08-10戴维标

江苏第二师范学院学报 2014年11期

关键词：程序开发编程语言契约

戴维标

(盐城工学院继续教育学院，江苏盐城 224051)

基于契约式设计的VeriJava编程语言设计

戴维标

(盐城工学院继续教育学院，江苏盐城 224051)

契约式设计是一种以Java语言为主流编程的技术手段，无论是在VeriJava编程语言程序开发中，还是在C++、S#等语言开发中，都被程序开发者广泛使用.对VeriJava编程语言以契约式设计理论的程序设计进行分析研究，将契约式设计理念引入到面向对象编程技术开发中,从而实现契约的编写与程序分离.

契约式设计理念；VeriJava编程语言设计；Java语言

契约式设计是指面向对象程序中的类与客户之间关系的一种形式化约定，主要包括前置条件、后置条件和不变式，在面向对象程序中，只有明确了定义模块之间的权利和职责，才能构建高质量、高可靠性的大型软件系统，本文则通过设置契约来约束程序行为的新型语言系统——VeriJava，从而实现VeriJava程序的动态检查.

1 契约式设计理论分析

在面向对象程序中，契约式设计要求客户与提供者之间需遵循契约的规定[1]，其明确定义模块之间的权利者职责，主要包括前置条件、后置条件和不变式，前置和后置条件都是针对某个方法的，即前置条件(precondition)必须满足该方法被调用之前的条件，而后置条件(postcondition)必须满足该方法被调用之后的条件，然而，不变式(invariant)是针对类的，其主要描述这个类的全局属性，并且类的所有调用方法都必须满足不变式.

分析契约式设计理论，是一种构建高可靠软件并将面向对象程序中的类及客户之间的关系作为一种形式化约定的系统化方法，然而，在形式化的基础上，其需要明确类及客户之间的权利和职责，而类及客户模块之间定义的约定则被称为“契约”.为了构建高质量、可靠性的软件系统，在实践中，还需要使用规范说明(specification)，为系统化的测试和排错提供良好的基础，一般要求每一单元都要使用一个规范说明.在程序开发中使用规范说明，不仅可以为程序开发人员提供参考，也可以通过静态验证的定理证明来确保程序的正确性，因此，在程序开发中引入契约式设计理论，不仅可以让人们更好地理解面向对象的方法和软件构造，还可以更好地理解和控制继承机制，是一种安全、高效处理程序异常的技术[2].

2 VeriJava编程语言概述

在面向对象软件程序开发中，最为直观、有效的形式属于程序开发人员直接编写契约.由于Java是一种面向对象的高级语言，虽然其具有实现多个接口、动态分配方法等特性，但其类只能从一个父类进程，而VeriJava是Java编程语言的拓展语言，VeriJava编程语言设计的主要目标是令Java语言通过支持契约具有可验证性，这就需要提供静态验证、动态检查的程序接口，并且需要为VeriJava提供基本的编辑器和动态验证器等工具支持.图1为 VeriJava 语言系统的整体架构图，从图中可以看出，VeriJava 语言系统的基础架构属于VeriJava 语言的定义与规范，通过构建编译器和利用动态检查工具作为整个面向对象编程的技术支撑，对基本的类进行封装，通过对程序设计进行静态验证，这样就可以通过定理证明对基于契约式设计编写的程序进行验证[3].

图1 VeriJava 语言系统的整体架构

3 VeriJava语言程序设计分析

3.1 在VeriJava程序设计中契约条件的支撑

VeriJava编程语言是一种作为扩展Java语言支持契约式设计的语言系统.契约分为类、非空类型及方法等三种契约类型.第一，方法契约类型，主要表达语言执行前后的状况，其局限于它所限定的某个特定方法.第二，类契约，契约的作用范围为整个类的范围，即在对象生存周期中需要定义特殊的时间点及常量契约的校验；第三，非空类型契约，主要针对契约中的特殊条件的契约类型，在契约规定中，一般要求非空类型契约的类的初始化值需要有参数，而不能为空，并且在类声明中，也需要有某种形式的域，除特殊对象外，一般类的创建都需要采用 new操作符后面加上构造类型的模式来实现，在提供构造器过程中，必须提供初始化参数，这样才能在编译过程中作用于构造器的约束[4].

3.2 VeriJava编程语言词法、语法、语义定义

通过在原有Java支持的契约条件的基础上来制定出VeriJava语言系统的基本规范，其中，定义词法、语法和语义是语言系统的基础，在定义语言，最为规范的则是利用BNF范式来定义词法和语法，BNF范式是支持以迭代的方式进行验证.由于VeriJava设计支持方法契约、类契约和非空契约等三个方面的契约条件，其不仅为对象中的属性增加约束，也为方法增加了以前置和后置条件为基础的契约，针对VeriJava编程语言的定义，其主要是在Java语法特性上进行定义，在语法定义中通常采用递归定义的方式，其是BNF范式中的方法，如方法契约的定义：

=???

= < REQUIRES_STATEMENT >

= requires

= ensures

= signals

= modifies

= ?

= $return

= old( )

一般情况下，语义定义的说明需要利用所有契约的通式进行说明，并且所有的契约条件都是由布尔表达式构成的，包括前置条件，后置条件及常量等，所以，利用Java布尔表达式进行语言编写，在包含多个条件的情况下，可以利用&符号将多个条件连接.从方法契约定义中，可以知道方法契约主要由前置条件、后置条件和框架条件构成，在不制定的情况下，则说明无需校验满足契约.在程序编写中，在契约方法无副作用情况下，VeriJava允许利用含有契约的方法来进行契约的编写，若利用VeriJava语言本身的表达式来编写契约，则可能会出现校验契约表达式出现错误的情况.一般情况下，除private方法之外，方法契约都可以使用其他方法.另外，在方法契约中，还包括方法签名、方法声明等语义定义，引入方法契约后，这就需要对方法名的定义进行相应的修改，即方法声明之后，需要在之前加入方法契约[5].

例如，下面则是VeriJava 语言编写的代码，进而说明VeriJava的语言特性：

Package st.cee.java.aa;

Class Company{

Invariant employ Number>0; //常量

!String company Name； //非空类型声明

! Int employ1; //非空类型

Public Company() company Name=“Example Company”(employ Number=50) //构造器对非空类型的初始化

Public void recruit (int new Comer)

Requires new Comer>=0 //前置条件

Ensures old (employ Number)

Modifies this.employ Number{

employ Number+=new Comer;

}

3.3 在VeriJava语言编程设计中的动态检查分析

分析契约校验的类型主要分为静态和动态两种契约检查类型，针对静态的契约检查，由于静态验证包含在静态编译器的范围之内，这就需要利用编译器来完整契约校验.因此，本文则重点分析动态的执行期契约检查.动态检查主要是利用契约动态检查的工作原理进行某个转换程序的转换，通过将契约条件转换为符合面向对象的Java语句，并对断言语句进行判断，若契约条件检验失败，系统将以异常的形式将错误信息报告给程序开发人员.在动态检查中，采用面向方面的编程的实现方式，其简称为AOP，将面向方面编程的实现方式应用在动态检查中，不仅可以充分体现出代码的灵活性，也可以明确表达设计的程序与类中组件之间契约.图2表示基于AOP的契约动态检查，分析面向方面的编程(AOP)的概念，对于AOP中的切面(Aspect)，其是对象操作过程中权限检查、日志、事物处理等截面，对于AOP中的Advice，则主要是对某个连接点所采用的处理逻辑，在Java领域中，最为成熟的则属于Aspect技术.在契约动态检查中，其主要发生在程序执行到某些特性的阶段，契约动态检查实际上是一种横切关注点分离的方式.比如面向对象语言中某个对象的调用，在调用之前，首先应对契约中的前置条件、后置条件和常量进行校验，程序开发人员可以在单独的模块中利用面向方面的编程技术来编写语言，充分利用契约中的声明条件.采用面向方面的编程技术，不仅优化了横切关注点的建模，也方便程序开发人员对系统进行合理设计、理解和维护，提高代码的产量和质量，使AOP技术更有益于实现追加的特性.