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

[摘 要]：文章定义了VeriJa语言系统的语法和词法,并将契约式设计条件实现,对于实践而言,以ECLIPSE插件为基础,简要介绍了VeriJa开发工具包,实现了VeriJa程序利用开发工具即可创建.并在VeriJa插件工具包中集成了动态检查工具,可动态检查程序.

[关 键 词]：编程动态检查VeriJa契约式设计

随着网络信息化及计算机技术的不断飞跃发展,契约式设计理念被多种编程语言支持,其中,主流编程语言就是JA.为了使JA从语言级别对契约式设计形成支持,开发以契约编程为基础的模式,在保留JA原有特性前提下,扩展JA语言,于是诞生了VeriJa.契约式设计科提高对软件的可靠性.在契约式设计中,软件系统作为互相交流的部件,而部件相互之间的义务被定义为契约.

一、契约式设计的定义及其对程序开发的意义

契约式设计是一种设计计算机软件的方法,且构建的软件具有高可靠性与高质量,该方法对软件设计者提出要求,则为软件组件定义接口,且该接口是可验证、精确的、正式的.近些年来,无论是技术上还是理论上,契约式设计都取得了前所未有的成绩,受到工业领域和学术界的广泛关注,且契约式编程概念也随之诞生.JA平台也有了诸多不同的技术支持契约式技术,例如：JCONTRACTOR以及ICONTRACT等技术.将契约式设计引入程序中后,该设计的引入大幅增强了软件系统完备性和充实性,可通过契约式设计的引入优点来了解其深远意义.契约式设计不会混淆接口文档,书写清晰；可控制和减少调试产生的开销,利用监测可将错误及时发现；分离常规应用与契约检查,控制、降低测试成本；以契约式设计为基础实现异常情况的有效、安全处理；使人更好了解及操控继承机制；该设计能够给软件部件创建文档；确保质量,并且为测试、除错提供出高效率框架；深化软件构造和面向对象方法的理解.

二、VERIJA语言的设计、定义与特性

在对语义进行定义之前,应说明与契约条件相适用的通式,由布尔表达式构成常量、前置、后置这3种条件的.由框架条件、前置条件、后置条件共同构成了方法契约,方法契约由进行定义.若未指定三个元素,则说明无需对满足契约的情况进行校验.这样定义的好处是为了在VeriJa中JA程序不会因契约不足而不合法.在限定程序行为的同时,VeriJa语言中的方法契约自身不会将程序的状态改变.除了PRIVATE方法之外,方法契约适用于任何方法.通过扩展JA语言,VeriJa语言系统对语法和语义进行了全新定义,是契约式设计成为现实.在VeriJa语言的规定下,契约成为接口和类的一部分,布尔表达式能够实现契约条件的编写.对于原有的JA语法语义,VeriJa没有进行改写,这样设计时考虑到与JA程序更好兼容.

契约校验可在方法执行前后进行,这是契约式设计中最为关键的概念.方法契约被VeriJa定义全面覆盖.方法本身可被覆写或被重载,且拥有的标识符也不同,对此应对继承类结构进行考虑.以布尔表达式的形式,将契约表达式放置于方法体和方法签名之间.如果没有将子句编写上,那么后置条件与前置条件为true.方法契约并非适合所有方法,特别是PROTRCTED和PUBLIC方法会对其展开应用.因为PRIVATE方法是PROTECTED和PUBLIC方法的辅助实现,对外不可见,所以外界不会因此产生交互.

三、VERIJA工具包

以ECLIPSE插件技术为基础的开放式工具集合就是VeriJa工具包.工具包实现功能诸多,包括动态检查器、编辑器、视图、NATURE、向导等.VeriJa源文件及工程可通过VeriJa工具包来创建.VeriJa源文件的扩展名为vj,而命名规则相同于JA文件.因为BUILD扩展名已经在工具包中实现,因此在保存过程中,就会对VeriJa的编译器调用.ECLIPSE扩展点可实现新功能的添加.例如：想将新的一项内容加入菜单,可利用ECLIPSE扩点实现.该扩展点一旦实现,同时就建立一个扩展,不仅如此,该扩展还能创新建立属于自己的扩展点,由此得知,递归性是这种插件模式所特有的.通过不同扩展点,也能够不断实现VeriJa语言系统功能.工程类别属性的唯一标识就是NATURE,在.PROJECT文件中能够找到.在拥有多个NATURE属性的工程中导入与NATURE条件相符的工具或试图,且以vjnatrer为VeriJa的NATRER,在工程中导入VeriJa插件时,会对vjnatuer是否存在于该工程中进行检查,如果不存在,则无法使用VeriJa工具.

四、结束语

契约式设计是一种设计计算机软件的方法,将契约式设计引入程序中后,该设计的引入大幅增强了软件系统完备性和充实性,以契约式设计为基础实现异常情况的有效、安全处理；使人更好了解及操控继承机制.在限定程序行为的同时,VeriJa语言中的方法契约自身不会将程序的状态改变.方法契约被VeriJa定义全面覆盖.方法本身可被覆写或被重载,且拥有的标识符也不同,对此应对继承类结构进行考虑.以布尔表达式的形式,将契约表达式放置于方法体和方法签名之间.对VeriJa工具包的不断优化及完善有助于深入分析.通过工具包的建立,为研究VeriJa程序提供支持.应用该工具便于VeriJa程序的创建及编写.与此同时,VeriJa工具包还整合了插件,如动态检查工具,软件研发人员可直接动态验证程序.随着不断深入的契约编程研究,如描述面向对象的UML中引入契约式设计等,不断迎接新的挑战.