OO第三次单元总结

OO第三次单元总结

前言

第三单元的三次做业：JML规格化编程。根据已给的JML规格语言给出代码实现。

梳理JML语言的理论基础、应用工具链状况

JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言（Behavior Interface Specification Language，BISL），基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。JML主要由Leavens教授在Larch上的工做，并融入了BetrandMeyer， John Guttag等人关于Design by Contract的研究成果。近年来，JML持续受到关注，为严格的程序设计提供了一套行之有效的方法。经过JML及其支持工具，不只能够基于规格自动构造测试用例，并整合了SMT Solver等工具以静态方式来检查代码实现对规格的知足状况。

理论基础

JML以javadoc注释的方式来表示规格，每行都以@起头。有两种注释方式，行注释和块注释。其中行注释的表示方式为 //@annotation ，块注释的方式为 /* @ annotation @*/ 。
方法规格的核心内容包括三个方面，前置条件、后置条件和反作用约定。其中前置条件是对方法输入参数的限制，若是不知足前置条件，方法执行结果不可预测，或者说不保证方法执行结果的正确性；后置条件是对方法执行结果的限制，若是执行结果知足后置条件，则表示方法执行正确，不然执行错误。反作用指方法在执行过程当中对输入对象或 this 对象进行了修改（对其成员变量进行了赋值，或者调用其修改方法）。
\result表达式：表示一个非 void 类型的方法执行所得到的结果，即方法执行后的返回值。\result表达式的类型就是方法声明中定义的返回值类型。
\old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值。该表达式涉及到评估expr 中的对象是否发生变化，听从Java的引用规则，即针对一个对象引用而言，只能判断引用自己是否发生变化，而不能判断引用所指向的对象实体内容是否发生变化。
\forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每一个元素都知足相应的约束。
\exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素知足相应的约束。

应用工具链状况

openjml：使用SMT Solver来对检查程序实现是否知足所设计的规格。目前openjml封装了四个主流的solver：z3, cvc4, simplify, yices2。
JMLUnitNG/JMLUnit：根据规格自动化生成测试样例，进行单元化测试。

按照做业梳理本身的架构设计

第九次做业

类图：

复杂度分析：

第十次做业

类图：

复杂度分析：

阐述对规格撰写和理解上的心得体会