其他分享
首页 > 其他分享> > OO2019第三单元作业总结

OO2019第三单元作业总结

作者:互联网

写在前面

早在做第二单元的电梯作业时,便和同学开玩笑道,幸好没有让我们做地铁的排班、线路优化。没想到一语成谶,在第三单元地铁系统就迫不及待地跑来与我们相见。

JML语言基础及应用工具链

1.1 JML语言基础

JML是对java程序进行规格化设计的一种表示语言。它主要有两种用途:(1)开展规格化设计 (2)针对已有代码实现,书写规格,增加代码可维护性。

JML表达式

方法规格

类型规格

1.2 应用工具链简介

OpenJML:专门针对JML语言设置的验证工具,它可以检查JML规格语法的正确性,也可以根据方法的JML规格和具体实现来初步验证一个方法的实现是否其符合规格。

JMLUnitNG:可以自动生成测试数据来检验代码是否正确。

JUnit:单元测试工具,我们需要自己针对代码设置规范化样例。可以比较有针对性地检验单个方法的正确性。

 

SMT Solver:验证代码是否符合JML规范的工具

 

部署JML UnitNG

部署过程

  1. 从官方网站获取jar包:jmluniting-1_4.jar

  2. 运行命令:java -jar jmluniting-1_4.jar package/test.java

    (package 是 和jar包在同一级的文件夹,test.java是package文件夹下的待生成测试样例文件)

  3. 生成测试的文件如图,将其整个文件夹拷贝黏贴到idea工程中,运行test文件main方法,即可得到测试结果。

测试代码

/*@ public normal_behaviour
    @ ensures a >= b ==> \result == a;
    @ ensures b > a ==> \result == b;
    @*/
  public static int getBigger(int a, int b) {
      if (a >= b) {
          return a;
      } else {
          return b;
      }
  }

  /*@ public normal_behaviour
    @ ensures a <= b ==> \result == a;
    @ ensures b < a ==> \result == b;
    @*/
  public static int getSmaller(int a, int b) {
      if (a <= b) {
          return a;
      } else {
          return b;
      }
  }

  /*@ public normal_behaviour
    @ ensures \result == (a == b);
    @*/
  public static boolean isEqual(int a, int b) {
      return (a == b);
  }
   
  public static void main(String[] args) {
      getBigger(114514,1919810);
      getSmaller(3498,438373);
      isEqual(1,1);
      isEqual(334,473);
  }

 

测试结果

[TestNG] Running:
Command line suite

Failed: racEnabled()
Passed: constructor Demo()
Passed: static getBigger(-2147483648, -2147483648)
Passed: static getBigger(0, -2147483648)
Passed: static getBigger(2147483647, -2147483648)
Passed: static getBigger(-2147483648, 0)
Passed: static getBigger(0, 0)
Passed: static getBigger(2147483647, 0)
Passed: static getBigger(-2147483648, 2147483647)
Passed: static getBigger(0, 2147483647)
Passed: static getBigger(2147483647, 2147483647)
Passed: static getSmaller(-2147483648, -2147483648)
Passed: static getSmaller(0, -2147483648)
Passed: static getSmaller(2147483647, -2147483648)
Passed: static getSmaller(-2147483648, 0)
Passed: static getSmaller(0, 0)
Passed: static getSmaller(2147483647, 0)
Passed: static getSmaller(-2147483648, 2147483647)
Passed: static getSmaller(0, 2147483647)
Passed: static getSmaller(2147483647, 2147483647)
Passed: static isEqual(-2147483648, -2147483648)
Passed: static isEqual(0, -2147483648)
Passed: static isEqual(2147483647, -2147483648)
Passed: static isEqual(-2147483648, 0)
Passed: static isEqual(0, 0)
Passed: static isEqual(2147483647, 0)
Passed: static isEqual(-2147483648, 2147483647)
Passed: static isEqual(0, 2147483647)
Passed: static isEqual(2147483647, 2147483647)
Passed: static main(null)

===============================================
Command line suite
Total tests run: 30, Failures: 1, Skips: 0
===============================================

作业分析

第一次JML规格作业

架构设计

这次作业只根据官方接口实现了若干个类和方法,架构设计也非常简单,只有Main、MyPath、MyPathContainer三个类。类图如下。

MyPath类中的数据结构:

private ArrayList<Integer> pathNodes = new ArrayList<>();//存储一条路径的各个节点
private HashSet<Integer> disNodes = new HashSet<>();//存储不同的结点

MyPathContainer类中的数据结构,采用双向map减少查找路径时间:

private HashMap<Integer, Path> pid2path;//存储path的id和path的对应关系
private HashMap<Path, Integer> path2pid;//存储path和id的对应关系
private HashMap<Integer, Integer> containNodes;//存储每个结点及其出现的次数
private int current;//当前新增path的节点编号

bug分析和修复情况

本次作业没有出现bug。

发现bug的策略

与他人程序对拍;JUnit对每一个类,每一个方法实现针对性测试。

可能会出现bug的地方

这次作业CPU limit是10s,采用一些查找时间复杂度较高的容器类可能会超出CPU时间。

第二次JML规格作业

架构设计

本次作业基本上根据第一次作业的实现进行扩充,有Main、MyPath、MyGraph三个类。程序的类图如下

相比第一次作业,增加了几个容器,来描述节点是否相连,节点之间最短距离等特性。

bug分析和修复情况

本次作业没有出现bug。

发现bug的策略

与他人程序对拍;JUnit对每一个类,每一个方法实现针对性测试。

可能会出现bug的地方

这次作业我采用Floyd算法计算节点间的最短距离,每增加一条path时都需要重新建图。这时倘若采用静态数组,需要存储一下各个节点与其在数组中下标的对应关系。有同学因为将新增节点下标增加,造成了数组越界的情况。

第三次JML规格作业

架构设计

本次作业根据第二次规格作业进行扩充,有Main、MyPath、MyRailwaySystem、Floyd四个类。其中MyRailWaySystem根据新的要求在MyGraph的基础上进行了一些扩充。project的类图如下

为实现新增的四个方法要求,添加了Floyd类,在每添加一个path的时候,都为leastPrice,leastTransfer,leastUnpleasant三个方法重新建图,建图采用Floyd算法。

bug分析和修复情况

本次作业强测未出现bug。

但是在这次作业的课下测试阶段,由于设计思路有些不清晰,出现了如下bug,之后和同学交流,发现很多没有用拆点方法的同学在此处均出现了错误:

由于针对每个path采用Floyd算法单独建图,但这样要保证每个path的独立性,比如说在两条path中同时具有编号为16 30 20三个节点,在第一条path中16 与 30相连,第二条path中30 与 20 相连。这时两条path之间的节点间权值更新就可能会杂糅,最后的票价计算和不满意度计算出现错误。解决方法是,每条path单独初始化距离矩阵,之后再更新到总的距离矩阵中。

测试样例如下:

PATH_ADD 30 24 2 19 30 49 3 54 73 73 54 20 30
PATH_ADD 59 2 30 80 30 16 99 24 20 81 20
LEAST_TICKET_PRICE 20 16

发现bug的策略

与他人程序对拍;JUnit对每一个类,每一个方法实现针对性测试;构造一些极端数据(带环、自圈等等)进行测试。

可能会出现bug的地方

见上上part。

一点点心得

可能因为os逐渐硬核的os任务,老师、猪脚大大们的体谅,这三次作业难度稍有下降(除了令人头痛的第三次作业)。在这一单元中,我们初次接触了JML language ,首次使用JUnit对代码进行单元测试。

JML language是java建模语言,它就如我们os中的CML语言,能够对代码将要实现的功能进行描述,从而明晰设计思路,使写出来的代码更加美观,更符合规范,减少写出bug的可能性。但是设计JML语言规范往往需要花费更多的时间,也可能因为考虑不周出现一些规格设计上的错误,这些将有助于训练我们的思维全面性,也将有助于提高我们写代码的能力。

 JUnit是针对每一个方法进行单元测试的工具。在最开始接触到的时候,我错误地这东西没有什么用,效率不若直接测试,通读代码来得快。但是,随着设计越来越复杂,往往难以发现真正的bug出现在哪里,一但出现bug,想要通过调试找到它往往需要耗费大量的时间。此时,JUnit的强大功能便发挥出作用。针对可能出现错误的方法构造极端样例进行测试,往往能够使debug之路更加通畅。

最后,感谢老师猪脚们的辛勤付出,祝oo这一门课程越变越好~

标签:OO2019,2147483647,作业,JML,static,Passed,2147483648,bug,单元
来源: https://www.cnblogs.com/GeXiaoXiao/p/10904546.html