OO第三单元小结
第三次博客作业
一、梳理JML语言的理论基础、应用工具链情况
JML语言的理论基础：
JML为说明性的描述行为引入了许多构造。这些构造包括模型字段、量词、断言的可见度范围、前提条件、后置条件、不变量、合同继承以及正常行为与异常行为的规范。
将注释添加到Java代码中，这样我们就可以确定方法所执行的内容，而不需要关心具体的实现方法。
JML常见语法：
原子表达式 ：
\result：方法执行后的返回值。
\old(expr)：在相应方法执行前的取值。
量化表达式：
\forall：全称量词修饰的表达式。
操作符：b_expr1<==>b__expr2或b_expr1<=!=>b_expr2：等价关系操作符。
b_expr1==>b_expr2或b_expr1<==b_expr2：推理操作符。
方法规格：
requires ：前置条件。
ensures:后置条件。
public normal_behavior和public exception_behavior：方法的正常功能行为和异常行为。
signals (Exception e) b_expr：满足某个条件抛出相应异常。
signals_only (Exception e)：满足前置条件抛出相应异常。
应用工具链：有许多支持检验是否满足JML规格的工具，比如JMLUnit可以检查方法内代码是否满足JUnit约束；JUnit可以支持对单个方法的检验与测试；
SMT Solver可以验证程序的等价性。
三、部署JMLUnitNG/JMLUnit，针对Graph接口的实现自动生成测试用例， 并结合规格对生成的测试用例和数据进行简要分析
（不知道为什么用openJML后总是报错orz，弄好了之后再编辑一下）
四、按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构
第一次作业：
实现了两个类，Path和PathContainer。前者实现一条路径，后者则将多条路径加入到一个路径中，对总体路径情况进行更改和统计。
其中，Path中node采用ArrayList存储，重写equals和hashcode。PathContainer使用两个Hashmap存储pid和path，查找复杂度为O(1)，另外有一个Hashmap<Integer,Integer>存储总结点个数及其出现次数。
第二次作业：
没有使用继承，实现了两个类Path和Graph（涵盖了PathContainer的方法）。
采用了邻接压缩矩阵的方法存储整个图，即HashMap<Integer, HashSet<Integer>> graph，与第一次作业中的结点类似，将边存储到Hashmap中。
每次增删路径时，调用floyd()对任意两点之间的最短路径进行更新。另外还将最短路径存储到缓存中去，方便查找。floyd中为了简便计算，使用了二维数组。
floyd算法详细如下：
```private void floyd() {
```
for (int i = 0; i < vnum; i++) {
for (int j = 0; j < vnum; j++) {
dist[i][j] = Float.POSITIVE_INFINITY;
}
}
for (Map.Entry<Integer, HashSet<Integer>> entry : graph.entrySet()) {
HashSet<Integer> tmp = entry.getValue();
int idxX = nodeList.get(entry.getKey());
for (Integer y: tmp) {
int idxY = nodeList.get(y);
dist[idxY][idxX] = 1;
dist[idxX][idxY] = 1;
} for (int k = 0; k < vnum; k++) {
for (int i = 0; i < vnum; i++) {
for (int j = 0; j < vnum; j++) {
float tmp;
if (dist[i][k] == Float.POSITIVE_INFINITY
|| dist[k][j] == Float.POSITIVE_INFINITY) {
tmp = Float.POSITIVE_INFINITY;
}
else {
tmp = (dist[i][k] + dist[k][j]);
}
if (Float.compare(dist[i][j],tmp) > 0 && i != j) {
dist[i][j] = tmp;
dist[j][i] = tmp;
}
}
}
}
//update shortpaths
shortPaths = new HashMap<>();
for (int i = 0; i < vnum; i++) {
for (int j = 0;j < vnum; j++) {
if (dist[i][j] != Float.POSITIVE_INFINITY) {
int x = indexList.get(i);
int y = indexList.get(j);
shortPaths.put(new Position(x,y),(int)dist[i][j]);
}
}
}
}
其中，对于寻找最小路径的方法采用了floyd算法，每次增删路径时会对存储的floyd矩阵进行更新。
第三次作业：
使用了Edge、Node、CalculatePaths、Path和MyRailwaySystem类，实现了图的计算与地铁系统的分离，不足之处在于图的存储没有跟RailwaySystem很好的实现分离。
MyRailwaySystem只需要对总graph中所存储的edge和path进行更新，其余计算结果均从CalculatePaths中取出。
在CalculatePaths中封装了dijstra算法，传入不同需求的初始图，每次增删路径更新初始图，每次查找最短路径时进行更新。同时用四个压缩矩阵：shortPaths，pleasant，price，transTimes存储已经计算好的两点之间的最短距离。
对于初始图，刚开始我使用了(fromNodeId,toNodeId,fromPathId,toPathId,Weight)的方法实现Edge类，以PathId=-1为起点开始寻找乘坐起点所在的路径，并最终到达终点为止。这样需要在dijstra算法内部进行是否换乘的判断，但是这样并不能求解出正确的最短路径。
于是传入初始图时进行了更改，进行了讨论区里拆点的操作。下面是dijstra的详细实现：
private HashMap<Position,Integer> dijstra(
LinkedHashMap<Integer, ArrayList<Edge>> initial, int start,
HashMap<Position,Integer> result) {
PriorityQueue<Vedge> queue = new PriorityQueue<>();
int count = 0;
int vnum = nodes.size();
HashMap<Integer,Prior> paths = new HashMap<>();
queue.add(new Vedge(new Edge(start,start,startPath,startPath),0));
while (!queue.isEmpty() && count < vnum) {
Vedge cur = queue.poll();
int index = cur.getEdge().getEdge().getTo();
if (paths.get(cur.getEdge().getEdge().getTo()) != null) {
continue; }
paths.put(cur.getEdge().getEdge().getTo(),
new Prior(cur.getEdge().getEdge().getFrom(),
cur.getValue()));
if (initial.get(index) != null) {
for (Vedge tmp : initial.get(index)) {
if (paths.get(tmp.getEdge().getEdge().getTo()) == null) {
int var = cur.getValue() + tmp.getValue();
if (cur.getEdge().getFromNodeId() != -1) {
Vedge re = new Vedge(
new Edge(tmp.getEdge().getEdge().getFrom(),
tmp.getEdge().getEdge().getTo(),
cur.getEdge().getFromNodeId(),
tmp.getEdge().getToNodeId()), var);
queue.add(re); }
else {
Vedge re = new Vedge(
new Edge(tmp.getEdge().getEdge().getFrom(),
tmp.getEdge().getEdge().getTo(),
tmp.getEdge().getFromNodeId(),
tmp.getEdge().getToNodeId()), var);
queue.add(re); }
}
}
}
count++;
}
for (Integer key: paths.keySet()) {
Position tmp = new Position(start,key);
if (result.get(tmp) == null) {
result.put(tmp, paths.get(key).getPlen());
}
else {
result.put(tmp,Math.min(paths.get(key).getPlen(),result.get(tmp)));
}
Position tmp2 = new Position(key,start);
if (result.get(tmp2) == null) {
result.put(tmp2, paths.get(key).getPlen());
}
else {
result.put(tmp2,Math.min(paths.get(key).getPlen(),result.get(tmp2)));
}
}
return result;
}五、按照作业分析代码实现的bug和修复情况
第一次：没有发现bug。
第二次：没有考虑node与自身的连点，导致floyd中自身不可达，计算最短路径和连通性出错。
即初始化二维数组的时候，没有判断nodeId == nodeId的情况。
第三次：直接使用dijstra算法，在内部判断换乘，没有取得正确的最优解；对第二次作业进行了重构，删除路径时删了pidtoPath但没有暂存pathid，导致了NullPointerException。
对第二次作业进行了重构，重写了MyPathContainer，新增了HashMap pidToPath中，删除路径时没有对Path进行暂时存储，导致报错PathIdNotFoundException；此外，第一次采用的算法对换乘处理过于粗糙，换乘在dijstra内部判断，局部寻求最优解很有可能正确性没有达到。于是传入的初始化图进行了更新。
六、阐述对规格撰写和理解上的心得体会
有了规格之后具体实现就容易多了。只需要关心方法前后的状态变化，却不需要知道内部实现方法，通过检查前后置条件、不变式、状态变化约束等等，可以直接对程序的正确性进行评价判断。采取单元测试的方法，可以精确定位bug，测试更为规范化公式化。另外，特别是第三次作业，要做到不同类之间的分离，在railwaySsystem中直接进行图的计算是冗杂的设计。
优质内容筛选与推荐>>1、MyEclipse的项目中把 java EE 5 Libraries 删掉后怎么重新导入
2、用Java实现在【520,1314】之间生成随机整数的故事
3、俱乐部LOGO和T恤征集完毕
4、extjs4.0的文件导入
5、年级-专业编号-序号