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

阅读量：6581 次

发布时间：2019-06-24

本文共 5157 字，大约阅读时间需要 17 分钟。

概述

本单元主要学习规格化的面向对象设计方法，即使用行为接口规格语言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求出对应的结果即可。