OO第三单元总结

Posted okawaikoto

tags:

篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了OO第三单元总结相关的知识,希望对你有一定的参考价值。

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再实现对应类或方法,可以明确方法的边界行为,并对降低程序的耦合度很有帮助。而本次作业的迭代开发的过程,也让我对继承的具体实现有了更多的认识。

以上是关于OO第三单元总结的主要内容,如果未能解决你的问题,请参考以下文章

oo第三单元总结

OO第三单元总结

OO第三单元总结

OO第三单元总结

OO第三单元总结

OO第三单元总结