OO第三单元总结

Posted 2021-12-02 okawaikoto

OO第三单元总结

一. JML语言

理论基础

? JML是用于对Java程序进行规格化设计的一种表示语言

1. 注释结构

   JML以javadoc注释的方式来表示规格，每行都以@起头。有两种注释方式，行注释和块注释。其中行注释的表示方式 为//@annotation，块注释的方式为/* @ annotation @*/。按照Javadoc习惯，JML注释一般放在被注释成分的 近邻上部

2. JML表达式

   2.1 原子表达式：

   \result表达式：表示一个非void类型的方法执行所获得的结果，即方法执行后的返回值

   \old( expr )表达式：用来表示一个表达式expr在相应方法执行前的取值。

   \not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。

   \not_modified(x,y,...)表达式:该表达式限制括号中的变量在方法执行期间的取 值未发生变化。

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

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

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

   2.2 量化表达式

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

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

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

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

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

   2.3 集合表达式

   集合构造表达式：可以在JML规格中构造一个局部的集合（容器），明确集合中可以包含的元素。

   2.4 操作符

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

   (1) 子类型关系操作符：E1<:E2

   (2) 等价关系操作符：b_expr1<==>b_expr2或者b_expr1<=!=>b_expr2

   (3) 推理操作符：b_expr1==>b_expr2或者b_expr2<==b_expr1。

   (4) 变量引用操作符：\nothing指示一个空集；\everything指示一个全集

3. 方法规格

   • 前置条件： requires p;
   • 后置条件： ensures p;
   • 负作用范围限定： 可以更改的数据，使用assignable表示
   • 异常行为：需要抛出的异常，用signals子句表示。

应用工具链

• OpenJML：检查JML中使用规范注释的Java程序正确性。
• JMLUnitNG：基于JML注释的Java代码的自动化单元测试生成工具。

二. 部署JMLUnitNG

 public class Sub {
 2     /*@ public normal_behaviour
 3       @ requires a > 0 && b > 0;
 4       @ ensures \result == a - b;
 5       @*/
 6     public static int sub(int a, int b) {
 7         return a - b;
 8     }
 9 
10     public static void main(String[] args) {
11         sub(1, 1);
12     }
13 }

　首先，对JML语言进行检查。

1 java -jar ../openjml/openjml.jar -check Sub.java > re.txt

生成和编译

1 java -jar jmlunitng-1_4.jar Sub.java 
2 javac -cp jmlunitng-1_4.jar *.java
3 java -jar ../openjml/openjml.jar -rac Sub.java
4 java -cp jmlunitng-1_4.jar Sub_JML_Test

运行结果如图：

三. 架构设计

第一次作业：

第一次作业要求为实现容器类Path和PathContainer，Path为节点序列，PathContainer需要实现pathid和path的检索以及容器内不同节点个数的查询。

具体实现为：Path类通过Arraylist存储路径，Hashset存储点集；PathContainer通过两个Hashmap解决路径检索，维护一个Hashmap记录不同节点的个数。

第二次作业：

在第一次作业的基础上要求实现Graph类，需要实现对任意节点间最短距离的查询。

我实现了GraphQuery类来完成对所有图相关查询指令的处理。最短距离的计算，我选择使用floyd法，由于节点的id为int类型，需要首先将其映射到从0开始的连续整数。在GraphQuery中维护一个Hashmap记录该映射关系。每次增加路径时，Graph类调用GraphQuery的add方法，为新增的所有新节点分配映射关系，初始化floyd矩阵并计算。每次删除路径时，重新初始化floyd矩阵并计算。

第三次作业：

在第二次作业的基础上要求实现RailwaySystem类，实现对任意节点间最少换乘、最少票价和最少不满意度和图的联通块数目的查询。

图的联通块数目我采用bfs染色进行计算。

对于三种最短路的计算，我采用讨论区著名的wjy算法，将每一条路径先构造成完全图，对于最少换乘，将一条路径上所有点间的权值设为1；对于最少票价，则将权值设为两点间的距离+换乘费用也就是2；对于最少不满意度，将权值设为两点间的不满意度+换乘不满意度即32；如此对任意查询，求其对应图的两点间最短路径即可。

具体架构：由于每条路径都需要重新建图，且该图是稀疏图，因此我采用spfa法计算对不同查询要求计算两点间的新权值。首先封装了SpfaCalculator用于对一张图的最短距离计算，每增加一条路径，实例化一个Updater，记录该路径对应的邻接矩阵并调用SpfaCalculator计算，返回新图。在RailwayQuery中维护三个矩阵分别对应三种需求，对每一条路径，调用updater获取小图并更新大图，之后进行floyd运算。

四. bug和修复情况

第一二次作业均没有bug出现，第三次作业对相同节点的contains edge出了问题，通过floyd矩阵中对应位置元素的大小是否为1来判断，但在初始化该矩阵时跳过了对角元的初始化，导致总是返回无穷大。

五. 心得体会

JML语言更加精准的描述了一个类或者方法的行为，先写JML再实现对应类或方法，可以明确方法的边界行为，并对降低程序的耦合度很有帮助。而本次作业的迭代开发的过程，也让我对继承的具体实现有了更多的认识。