论文部分内容阅读
摘 要:实现了一个C#语言的合约检查工具,用于辅助程序员在用C#语言编写软件的时候运用合约式设计方法。工具将书写在程序注释中的合约提取出来,并转化为类不变式、类方法的前置条件或后置条件的检查代码插入到源文件中。当执行含有合约检查代码的源文件的时候,检查代码将被执行,以确保合约是否被遵守。
关键词:易测试性;合约式设计;类不变式;前置条件;后置条件
中图分类号:TP311文献标识码:A
The Research for Contract Wrapper Based on C# Language
LI Ying-na
(Kunming University of Science and Technology,Yunnan Kunming 650051)
Key words: testability;design by contract;class Invariant;precondition;postcondition
软件业的飞速发展,使各行业对软件的依赖性也日益增加。这种依赖,导致软件的使用者对软件的要求越来越高,软件需求更加细致和独立。软件制造业正面临着一些新的课题,如复杂的分布环境、灵活的应用模式、广泛的包容性等,传统的软件设计思想已远远不够。
面向构件的设计模式为大规模、集成化软件设计带来了极大便利,同时也带来了更多的问题。特别是组成一个新系统的构件的协同性和互操作性问题。合约式设计(Design By Contract)把类和它的客户程序之间的关系看作正式的协议,描述双方的权利和义务。B. Meyer把它称作构建面向对象软件系统方法的核心。B.Meyer在Object-Oriented Software Construction一书中讲到:“对于一个大型系统来说,光保证它的各组成部分的质量是不够的。而最有价值的是确保在任何两个组成部分的交接处设计明晰的彼此义务和权利规范,即所谓合约。”DbC的提出,主要基于软件可靠性方面的考虑。在整个软件过程中,从概念模型的business use case用例规约开始就会有很多前置、后置条件,这些条件被具体化到设计模型后,就是每个对象元素的合约了。
1 实现内容
本文从合约化构件设计入手,实现一个基于C#语言的合约式软件开发工具,在C#语言的基础上,增加支持合约式设计的语法,并能与现有的开发平台(.NET)实现良好的对接,实现支持合约的构件化开发。
本工具主要功能除支持几种主要类型的合约:前置条件、后置条件、类不变式之外,同时还支持循环变式、循环不变式、量词等。
合约式设计中将这些条件集中明确的声明,确定职责归属,并由框架辅助进行验证。为了使工具更加的方便实用,更好地发挥合约式设计的优势,在认真的分析了已有的各种基于C#语言的合约检查工具的利弊的基础上,我们提出了工具需求如下:
合约检查非强制性设计;不进行合约的嵌套检查;合约的描述:除C#语法本身支持的表达式外,在合约中增加全称量词、循环量词,并能够表达蕴涵关系。增加合约关键子,继承和完善C#中断言Assertion的功能;支持合约的继承:合约的继承包括类不变式的继承、前置条件的继承、后置条件的继承;
注释的描述形式:合约采用注释的形式出现在C#源文件中。所有合约实现的语句全部定义在注释//和/**/中,并以#开头;
2 工具的设计方案
工具的任务是从含有合约的C#源文件中提取合约并对合约进行词法和语法检查,并根据语义在C#源文件中进行合约位置的搜索和插装,形成符合C#语法的代码,该代码可以在诸如.NET平台上进一步优化编译成目标代码。
2.1词法和语法分析器的实现
ANTLR是ANother Tool for Language Recognition的缩写,其功能是根据给定文法自动生成编译器,本项目采用ANTLR作为主要的开发工具,使用了类似EBNF(Extended Backus-Naur Form)的文法定义方式,需要时也可以利用ANTLR快速实现基于JAVA或C++等语言的DbC工具。
2.1.1合约部分的词法和语法的ANTLR文法
/*注释部分词法,$channel=HIDDEN 表示注释在词法分析时放入隐藏频道,以备语法分析时使用*/
COMMENT :'/*' . *'*/' {$channel=HIDDEN;} ;
LINE_COMMENT : '//'~ ('\n' | '\r') *'\r'? '\n' {$channel=HIDDEN;} ;
/*定义合约部分的语法*/
method-list:method+;
//定义合约的位置
method : method-name [ '('para-list')' ] returns return-type
contract-spec;
//合约种类的定义,合约都在包含在多行注释:/**/之间的。
contract-spec:
/*PreconditionSection|PostconditionSection|InvariantSection|LoopSection|notnullSection*/;
PreconditionSection:#pre [pre-name:] ContractExpression ; //前置条件的定义
PostconditionSection:#post [post-name:] ContractExpression ; //后置条件的定义
InvariantSection:#invariant [invar-name:] ContractExpression;//类不变式的定义
//循环变式(不变式)的定义
LoopSection: #loop [loop-name] from (statement)?
(invariant expression)|(variant expression)
until ContractExpression
loop { statement }
End;
NotnullSection:#! type ! variable; //非空变量的定义
//合约表达式的定义,是合约的主要组成部分。
ContractExpression:
expression //一般的Boolean表达式
| forall type VariableDeclarator in collection expression//forall表达式(全称量词)
|exists type VariableDeclarator in collection expression//exists表达式(存在量词)
|expression implies expression; //implies表达式(蕴涵表达式)
collection:(element)+; //集合表达式
element:
integer-literal …integer-literal |character-literal …character-literal
|integer-literal| floating-point- type | character-literal | string-literal;
其中的黑体的为终结符,引用到的非终结符Expression, Type,VariableDaclarator等为C#语法规范中定义的一致;integer-literal、character-literal、floating-point-type、string-litera分别为整形、字符、浮点和字符串字面。
2.1.2对ANTLR生成代码的引用
用ANTLRWorks生成代码,这时目录中会生成三个文件“*Lexer.cs”、“*Parser.cs”、“*.tokens”,其中“*”是“*.g”文法文件的主文件名。*Lexer.cs为词法分析器,*Parser.cs为语法分析器。
在.NET开发中先新建一个C# WindowApplication项目,将上述生成的文件拷贝并加入到项目中。再将.NET版的ANTLR Runtime的DLL引用到项目中来。本示例需要Antlr3.Runtime.dll和antlr.runtime.dll,这两个文件在antlr-3.1.3.tar.gz解压后的antlr-3.1.3\antlr-3.1.3\ runtime\CSharp\bin\net-2.0目录中可以找到。这些操作都完成之后,在窗体的代码文件Form1.cs中加入:
using Antlr.Runtime;
using Antlr.Runtime.Tree;
编写相应的运行代码编译,添加相关表达式的实现类,这个编译器就可以进行工作了。
2.2合约信息的提取
利用ANTLR生成的词法和语法程序,对含有合约信息的C#源文件进行词法和语法的分析,如果分析正确,将获得一个源文件的分析树。按照深度优先周游这颗分析树,在周游的过程中提取源文件的所有的信息。
周游分析树在ReflectVisitor类中完成,由于节点类型繁多所以实现采用了visitor模式。分析树中的任何一种节点类型在ReflectVisitor类中都存在一个与之对应的visit方法对该类型的节点进行访问,获得节点中的有用的信息,并将这些信息保存在已经设计好的结构中,这些结构包括表达式相关类、Class、Method等实体类,以及合约相关类Contract等,合约信息提取将为后面的合约正确性检查(主要是语义的正确性)以及合约的插装做好准备。
在周游的过程中需要保存前面周游的一些信息,采用了如下的结构:
public class VInfo {
public reflect.Class clazz = null; //记录当前所访问的节点所属的类
public reflect.Method method = null; //记录当前所访问的方法
/*记录当前访问的类的名字(含有包前缀修饰的全名)*/
public String unitName = null;
public Vector fields = new Vector();//记录当前所访问的类中所声明的属性
/*记录当前所访问的类中所声明的方法(不含构造方法)*/
public Vector methods = new Vector();
public Vector constructors = new Vector();//记录当前所访问的类中的构造方法
public Stack locals = new Stack();/记录当前方法中,节点可以访问的局部变量
public Vector forall_exists = new Vector();//保存forall/exits表达式
public int loopCounter = 0; //当前所访问的方法的循环计数
public int forallCounter = 0; //当前所访问的类中的forall/exits表达式计数
public boolean inMethod = false; //当前节点是否处于方法体中
public reflect.Class outerClass = null; //直接包含当前所周游类的外部类
public boolean inLoop = false; //记录当前是否处于循环体中
public boolean inContract = false; //当前节点是否是在合约中
}
2.3合约的插装
要正确插装合约,首先需要能够准确地定位合约插入的源文件位置。通过对分析树的周游方法确定插入的位置,能够保证位置的准确,因为所有的C#程序都是遵守C#文法规则的。此处使用的分析树同语法检查的时候使用的分析树为同一棵分析树,也同样将使用观察者模式,将生成合约部分代码放在一个类中。
3 结束语
本文在调研了许多现有的有关合约设计工具的基础上,分析它们的优缺点,由此提出了我们的合约检查工具的设计方案。只是工具目前仅提供命令行使用模式,依赖于其他环境完成编码工作,使用时不是很方便。下一步将开发一个IDE的编辑工具,使得用户能够在编辑工具里面很方便地添加合约,以及进行合约的适时检查。
参考文献:
[1]Bertrand Meyer. Object-Oriented Software Construction. Prentice Hall, Upper Saddle River, New Jersey, 1997.
[2]Bertrand Meyer. Design by Contract: The Lessons of Ariane. IEEE Computer,vol.30, no.1,January 1997,pp.129-130.
[3]ANTLR简介,http://alien1979.e34.163ns.com/Default.aspx
[4]单锦辉,一种基于合约的构件易测试性设计方法[D].第四届中国测试学术会议第四届中国测试学术会议(CTC 2006)论文集,2006.
[5]李敏波翻译. C#高级编程[M]. 第4版.北京:清华大学出版社,2006.
关键词:易测试性;合约式设计;类不变式;前置条件;后置条件
中图分类号:TP311文献标识码:A
The Research for Contract Wrapper Based on C# Language
LI Ying-na
(Kunming University of Science and Technology,Yunnan Kunming 650051)
Key words: testability;design by contract;class Invariant;precondition;postcondition
软件业的飞速发展,使各行业对软件的依赖性也日益增加。这种依赖,导致软件的使用者对软件的要求越来越高,软件需求更加细致和独立。软件制造业正面临着一些新的课题,如复杂的分布环境、灵活的应用模式、广泛的包容性等,传统的软件设计思想已远远不够。
面向构件的设计模式为大规模、集成化软件设计带来了极大便利,同时也带来了更多的问题。特别是组成一个新系统的构件的协同性和互操作性问题。合约式设计(Design By Contract)把类和它的客户程序之间的关系看作正式的协议,描述双方的权利和义务。B. Meyer把它称作构建面向对象软件系统方法的核心。B.Meyer在Object-Oriented Software Construction一书中讲到:“对于一个大型系统来说,光保证它的各组成部分的质量是不够的。而最有价值的是确保在任何两个组成部分的交接处设计明晰的彼此义务和权利规范,即所谓合约。”DbC的提出,主要基于软件可靠性方面的考虑。在整个软件过程中,从概念模型的business use case用例规约开始就会有很多前置、后置条件,这些条件被具体化到设计模型后,就是每个对象元素的合约了。
1 实现内容
本文从合约化构件设计入手,实现一个基于C#语言的合约式软件开发工具,在C#语言的基础上,增加支持合约式设计的语法,并能与现有的开发平台(.NET)实现良好的对接,实现支持合约的构件化开发。
本工具主要功能除支持几种主要类型的合约:前置条件、后置条件、类不变式之外,同时还支持循环变式、循环不变式、量词等。
合约式设计中将这些条件集中明确的声明,确定职责归属,并由框架辅助进行验证。为了使工具更加的方便实用,更好地发挥合约式设计的优势,在认真的分析了已有的各种基于C#语言的合约检查工具的利弊的基础上,我们提出了工具需求如下:
合约检查非强制性设计;不进行合约的嵌套检查;合约的描述:除C#语法本身支持的表达式外,在合约中增加全称量词、循环量词,并能够表达蕴涵关系。增加合约关键子,继承和完善C#中断言Assertion的功能;支持合约的继承:合约的继承包括类不变式的继承、前置条件的继承、后置条件的继承;
注释的描述形式:合约采用注释的形式出现在C#源文件中。所有合约实现的语句全部定义在注释//和/**/中,并以#开头;
2 工具的设计方案
工具的任务是从含有合约的C#源文件中提取合约并对合约进行词法和语法检查,并根据语义在C#源文件中进行合约位置的搜索和插装,形成符合C#语法的代码,该代码可以在诸如.NET平台上进一步优化编译成目标代码。
2.1词法和语法分析器的实现
ANTLR是ANother Tool for Language Recognition的缩写,其功能是根据给定文法自动生成编译器,本项目采用ANTLR作为主要的开发工具,使用了类似EBNF(Extended Backus-Naur Form)的文法定义方式,需要时也可以利用ANTLR快速实现基于JAVA或C++等语言的DbC工具。
2.1.1合约部分的词法和语法的ANTLR文法
/*注释部分词法,$channel=HIDDEN 表示注释在词法分析时放入隐藏频道,以备语法分析时使用*/
COMMENT :'/*' . *'*/' {$channel=HIDDEN;} ;
LINE_COMMENT : '//'~ ('\n' | '\r') *'\r'? '\n' {$channel=HIDDEN;} ;
/*定义合约部分的语法*/
method-list:method+;
//定义合约的位置
method : method-name [ '('para-list')' ] returns return-type
contract-spec;
//合约种类的定义,合约都在包含在多行注释:/**/之间的。
contract-spec:
/*PreconditionSection|PostconditionSection|InvariantSection|LoopSection|notnullSection*/;
PreconditionSection:#pre [pre-name:] ContractExpression ; //前置条件的定义
PostconditionSection:#post [post-name:] ContractExpression ; //后置条件的定义
InvariantSection:#invariant [invar-name:] ContractExpression;//类不变式的定义
//循环变式(不变式)的定义
LoopSection: #loop [loop-name] from (statement)?
(invariant expression)|(variant expression)
until ContractExpression
loop { statement }
End;
NotnullSection:#! type ! variable; //非空变量的定义
//合约表达式的定义,是合约的主要组成部分。
ContractExpression:
expression //一般的Boolean表达式
| forall type VariableDeclarator in collection expression//forall表达式(全称量词)
|exists type VariableDeclarator in collection expression//exists表达式(存在量词)
|expression implies expression; //implies表达式(蕴涵表达式)
collection:(element)+; //集合表达式
element:
integer-literal …integer-literal |character-literal …character-literal
|integer-literal| floating-point- type | character-literal | string-literal;
其中的黑体的为终结符,引用到的非终结符Expression, Type,VariableDaclarator等为C#语法规范中定义的一致;integer-literal、character-literal、floating-point-type、string-litera分别为整形、字符、浮点和字符串字面。
2.1.2对ANTLR生成代码的引用
用ANTLRWorks生成代码,这时目录中会生成三个文件“*Lexer.cs”、“*Parser.cs”、“*.tokens”,其中“*”是“*.g”文法文件的主文件名。*Lexer.cs为词法分析器,*Parser.cs为语法分析器。
在.NET开发中先新建一个C# WindowApplication项目,将上述生成的文件拷贝并加入到项目中。再将.NET版的ANTLR Runtime的DLL引用到项目中来。本示例需要Antlr3.Runtime.dll和antlr.runtime.dll,这两个文件在antlr-3.1.3.tar.gz解压后的antlr-3.1.3\antlr-3.1.3\ runtime\CSharp\bin\net-2.0目录中可以找到。这些操作都完成之后,在窗体的代码文件Form1.cs中加入:
using Antlr.Runtime;
using Antlr.Runtime.Tree;
编写相应的运行代码编译,添加相关表达式的实现类,这个编译器就可以进行工作了。
2.2合约信息的提取
利用ANTLR生成的词法和语法程序,对含有合约信息的C#源文件进行词法和语法的分析,如果分析正确,将获得一个源文件的分析树。按照深度优先周游这颗分析树,在周游的过程中提取源文件的所有的信息。
周游分析树在ReflectVisitor类中完成,由于节点类型繁多所以实现采用了visitor模式。分析树中的任何一种节点类型在ReflectVisitor类中都存在一个与之对应的visit方法对该类型的节点进行访问,获得节点中的有用的信息,并将这些信息保存在已经设计好的结构中,这些结构包括表达式相关类、Class、Method等实体类,以及合约相关类Contract等,合约信息提取将为后面的合约正确性检查(主要是语义的正确性)以及合约的插装做好准备。
在周游的过程中需要保存前面周游的一些信息,采用了如下的结构:
public class VInfo {
public reflect.Class clazz = null; //记录当前所访问的节点所属的类
public reflect.Method method = null; //记录当前所访问的方法
/*记录当前访问的类的名字(含有包前缀修饰的全名)*/
public String unitName = null;
public Vector fields = new Vector();//记录当前所访问的类中所声明的属性
/*记录当前所访问的类中所声明的方法(不含构造方法)*/
public Vector methods = new Vector();
public Vector constructors = new Vector();//记录当前所访问的类中的构造方法
public Stack locals = new Stack();/记录当前方法中,节点可以访问的局部变量
public Vector forall_exists = new Vector();//保存forall/exits表达式
public int loopCounter = 0; //当前所访问的方法的循环计数
public int forallCounter = 0; //当前所访问的类中的forall/exits表达式计数
public boolean inMethod = false; //当前节点是否处于方法体中
public reflect.Class outerClass = null; //直接包含当前所周游类的外部类
public boolean inLoop = false; //记录当前是否处于循环体中
public boolean inContract = false; //当前节点是否是在合约中
}
2.3合约的插装
要正确插装合约,首先需要能够准确地定位合约插入的源文件位置。通过对分析树的周游方法确定插入的位置,能够保证位置的准确,因为所有的C#程序都是遵守C#文法规则的。此处使用的分析树同语法检查的时候使用的分析树为同一棵分析树,也同样将使用观察者模式,将生成合约部分代码放在一个类中。
3 结束语
本文在调研了许多现有的有关合约设计工具的基础上,分析它们的优缺点,由此提出了我们的合约检查工具的设计方案。只是工具目前仅提供命令行使用模式,依赖于其他环境完成编码工作,使用时不是很方便。下一步将开发一个IDE的编辑工具,使得用户能够在编辑工具里面很方便地添加合约,以及进行合约的适时检查。
参考文献:
[1]Bertrand Meyer. Object-Oriented Software Construction. Prentice Hall, Upper Saddle River, New Jersey, 1997.
[2]Bertrand Meyer. Design by Contract: The Lessons of Ariane. IEEE Computer,vol.30, no.1,January 1997,pp.129-130.
[3]ANTLR简介,http://alien1979.e34.163ns.com/Default.aspx
[4]单锦辉,一种基于合约的构件易测试性设计方法[D].第四届中国测试学术会议第四届中国测试学术会议(CTC 2006)论文集,2006.
[5]李敏波翻译. C#高级编程[M]. 第4版.北京:清华大学出版社,2006.