面向对象程序设计第三单元总结

概述

本单元主要学习规格化的面向对象设计方法，即便用行为接口规格语言JML(Java Modeling Language)对Java程序进行规格化设计。其中咱们在课上实验上简要尝试了使用JML描述方法规格，课下做业主要是阅读已有框架和规格，而后按照规格编写方法完成程序。

JML语言

1.注释结构

JML以javadoc注释的方式表示规格，每行以@开头。有两种注释方式：

//行注释
//@annotation


//块注释
/*@ annotation @*/

2.JML表达式

2.1原子表达式

\result表达式：表示非void类型方法执行后的返回值。

\old(expr)表达式：用来表示一个表达式expr在相应方法执行前的取值。任何状况下，都应该使用\old把关心的表达式取值总体括起来，不然仅仅表示引用的地址是否发生变化，而不会表示引用的对象实体内是否发生变化。

\not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程当中被赋值。实际上，该表达式主要用于后置条件的约束表示上，即限制一个方法的实现不能对列表中的变量进行赋值。

\not_modified(x,y,...)表达式：与上面的\not_assigned表达式相似，该表达式限制括号中的变量在方法执行期间的取值未发生变化。

\nonnullelements(container)表达式：表示container对象中存储的对象不会有null。

\type(type)表达式：返回类型type对应的类型(Class)。

\typeof(expr)表达式：该表达式返回expr对应的准确类型。

2.2量化表达式

\forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每一个元素都知足相应的约束。

\exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素知足相应的约束。

\sum表达式：返回给定范围内的表达式的和。

\product表达式：返回给定范围内的表达式的连乘结果。

\max表达式：返回给定范围内的表达式的最大值。

\min表达式：返回给定范围内的表达式的最小值。

\num_of表达式：返回指定变量中知足相应条件的取值个数。通常的，\num_of表达式能够写成(\num_of T x;R(x);P(x))，其中T为变量x的类型，R(x)为x的取值范围;P(x)定义了x须要知足的约束条件。

2.3集合表达式

集合构造表达式：能够在JML规格中构造一个局部的集合（容器），明确集合中能够包含的元素。集合构造表达式的通常形式为：new ST{T x| R(x) && P(x)}，其中R(x)对应集合中x的范围，一般是来自某个既有集合中的元素。P(x)对应x取值的约束。

2.4操做符

JML表达式中能够正常使用java语言所定义的操做符，包括算术操做符、逻辑预算操做符等。此外，JML专门又定义了以下四类操做符：

（1）子类型关系操做符：E1 <: E2，若是类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，不然为假。若是E1和E2是相同的类型，则表达式的结果也为真。

（2）等价关系操做符：b_expr1 <==> b_expr2或者b_expr1 <=!=> b_expr2，其中b_expr1和b_expr2都是布尔表达式，这两个表达式的意思是b_expr1 == b_expr2或者b_expr1 != b_expr2。这两个表达式和java重的==和!=有相同的效果，按照JML语言定义，<==>比==优先级低，<=!=>比!=优先级低。

（3）推理操做符：b_expr1 ==> b_expr2或者b_expr2 <== b_expr1。

（4）变量引用操做符：除了能够直接引用java代码或者JML规格定义的变量外，JML还提供了几个归纳性的关键词来应用相关的变量。\nothing表示一个空集；\everything表示一个全集，即包括当前做用域下可以访问到的全部变量。

3.方法规格

方法规格的核心内容包括：前置条件、后置条件和反作用约定。

区分两类方法：所有过程和局部过程。前者对应着前置条件恒为真，便可以适应于任意调用场景；后者则提供了非恒真的前置条件，要求调用者必须确保调用时知足相应的前置条件。

区分两种调用场景：正常行为规格(normal_behavior)和异常行为规格(exceptional_ behavior)。

（1）前置条件(pre-condition)：前置条件是对方法输入参数的限制，若是不知足前置条件，方法执行结果不可预测，或者说不保证方法执行结果的正确性。经过requires子句来表示：requires P，requires是JML关键词，表示调用者确保P为真。方法规格中的多个requires子句为并列关系，即调用者必须同时知足全部的并列requires要求。若是想表达或逻辑，则应该使用requires P1 || P2

（2）后置条件(post-condition)：后置条件是对方法执行结果的限制，若是执行结果知足后置条件，则表示方法执行正确，不然执行错误。经过ensures子句表示：ensures P，ensures是JML关键词，表示方法实现者必须确保方法执行返回结果确保P为真。方法规格中的多个ensures子句为并列关系，即方法实现者必须同时知足全部的并列ensures要求。若是想表达或逻辑，则应使用ensures P1 || P2。

（3）反作用范围限定(side-effects)：反作用指方法在执行过程当中对输入对象或this对象进行了修改（对其成员变量进行了赋值，或者调用其修改方法），即方法在执行过程当中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响，因此必须明确给出反作用范围。JML使用assignable或者modifiable关键词来表示反作用的约束子句。

方法规格中还有一个关键词also，有两种使用also的场景：

（1）父类中对相应方法定义了规格，子类重写了该方法，须要补充规格，这时需在补充的规格以前使用also

（2）一个方法规格中涉及多个功能规格描述，正常功能规格或者异常功能规格，须要使用also

方法规格还包含signals子句，其结构为signals (Exception e) b_expr，意思是当b_expr为true时，方法会抛出括号中给出的相应异常e。

 

4.类型规格

 类型规格指针对java程序中定义的数据类型所设计的限制规则，通常说是指针对类或接口所设计的约束规则。JML主要设计两类限制规则，不变式限制(invariant)和约束显示(constraints)。类型规格都是针对类型中定义的数据成员所定义的限制规则。

（1）不变式(invariant)：不变式是要求在全部可见状态下都必须知足的特性，语法定义为invariant P,其中invariant为关键词，P为谓词。可见状态(visible state)有：

①对象的有状态构造方法(用来初始化对象成员变量初值)的执行结束时刻

②在调用一个对象回收方法(finalize方法)来释放相关资源开始的时刻

③在调用对象o的非静态、有状态方法(non-helper)的开始和结束时刻

④在调用对象o对应的类或父类的静态、有状态方法的开始和结束时刻

⑤在未处于对象o的构造方法、回收方法、非静态方法被调用过程当中的任意时刻

⑥在未处于对象o对应类或者父类的静态方法被调用过程当中的任意时刻

由上可看出，凡是回修改为员变量的方法执行期间，对象的状态都不是可见状态。

JML区分两种不变式：①静态不变式(static invariant)针对类中的静态成员变量取值进行约束②实例不变式(instance invariant)针对静态成员变量和非静态成员变量的取值进行约束。

（2）状态变化约束(constraint)：对象的状态在变化时也会知足一些约束，用constraint来对前序可见状态和当前可见状态的关系进行约束。JML也区分了两类约束：①static constraint：指涉及类的静态成员变量②instance constraint：涉及类的静态成员变量和非静态成员变量。

JML应用工具链状况

JML语言的工具链目前有不少，比较经常使用的是有，OpenJML能够用来检查JML的规范性，JMLUnitNG能够用来自动化生成测试数据，SMTSolver能够用来检查代码等价性。

 

三次做业分析

第一次做业

架构分析

实现细节

本次做业因为是继承官方接口，因此方法和接口一致，可是实现细节上，MyPath类利用了ArrayList存路径的点，用HashMap记录一条Path中不一样的点。MyContainer类利用两个HashMap构造了Path和PathId之间的双映射，便于path和pathId之间的互相查询，值得注意的是在利用path做为HashMap的索引时，要重写MyPath类的HashCode方法。而后还构建了一个HashMap用来存Container中不一样的结点。因为做业输入的指令绝大多数是查询指令，因此我在每次add和remove时更新要查询的数据，例如不一样结点数，而后每次查询时直接返回结果，而不用从新计算一遍，这样就极大下降了时间复杂度。

BUG分析

因为此次做业比较简单，在强测和互测中都未出现BUG。

第二次做业

架构分析

实现细节

第二次做业在第一次做业的基础上，增长了图的结构及和图有关的计算等要求。实现细节上，MyPath类和第一次做业没有任何变化。MyGraph类在MyContainer类的基础上，加入了图的结构相关的属性和方法。因为我是采用通常的二维数组的邻接矩阵来存图而不是邻接表来存图，而结点的值在Int范围以内，不能做为数组的下标，因此我构造了一个HashMap来表示结点和结点序号即数组下标之间的映射，并维护了一个Stack来存储当前可用的结点序号即数组下标。而后因为要实现图的结点间的最短路径的查询，我还创建了一个distance二维矩阵来存储每两个结点之间的最短路径。同第一次做业同样，此次做业也是查询指令占绝大多数，我在第一次做业add和remove的更改中，新添加了对于图和结点间的最短路径的更新，对于图的更新就是更新结点下标和邻接矩阵，更新结点间的最短路径就是经过bfs得到所有结点的最短路径而后记录下来。

BUG分析

此次做业虽然比第一次做业增长了有关图的相关运算，难度增长了一点，可是强测和互测依然没有被找出BUG。可是在完成做业时，本身找出了几个BUG，一个是在判断两个点之间是否有边时忘记判断这两个点是否存在于图中。另外一个是bfs时，忘记初始化距离矩阵，这就形成每次bfs都是在上一次的结果的基础上遍历的，会形成remove一条path以后，查询以前存在的而更新后不存在的结点间的距离时出错。

第三次做业

架构分析

 

实现细节

第三次做业在第二次做业的基础上，要求实现一个地铁系统的管理，并计算和地铁相关的最短换乘次数、最少票价和最少不满意度，实际上这三种计算都是最短路问题。在计算这些最短路时，我采起了不拆点的方法，但这要求在通常权重矩阵的基础上增长每两个点之间的权重，因此在MyPath类中，我把每一条Path都创建成了图，并经过Floyd算法求path内部的最少票价和最少不满意度，并用HashMap存储，当作外部访问的接口。而后MyRailwaySystem中，新增长了两个结点之间的最短换乘次数、最少票价和最少不满意度的存储矩阵以及对应的权重矩阵。而后在MyGraph的基础上，在每次add和remove时，更新最短换乘次数、最少票价和最少不满意度的权重矩阵，而后再利用Floyd求出对应的结果便可。

BUG分析

本次做业虽然在第二次做业的基础难度又上了一个台阶，可是在强测和互测上依然没有发现BUG。然而在写做业时，本身测试发现了三个BUG，是在计算最少票价、最少换乘次数和最少不满意度时没有判断两个结点相同时的状况致使出错。

感想体会

经过本单元的学习，我体会到了JML的好处，就是在进行代码架构的时候，对每一个类和每个方法进行约束，考虑正常和异常的状况，这样在撰写代码的时候，只要JML设计合理，在代码能正确完成JML的要求后，工程的正确性和稳定性能获得极高保障。