您的位置: 首页  >  文章  >  第三单元oo作业总结

第三单元oo作业总结

分类: 文章 • 2025-02-22 16:43:28

第三单元oo作业总结

第一部分：梳理JML语言的理论基础、应用工具链情况

理论基础 JML语法梳理

关于jml具体语法的梳理在给出的指导书中给出的基本上已经足够应用，以下为一部分常用语句的梳理。

  • 表达式：完成JML语句的编写
    • 原子表达式：如\result, \old(expr)等等
    • 量化表达式：如\forall表达式、\exists表达式等。
    • 集合表达式：通过集合表达式构造一个局部的容器，明确集合中包含的元素。
    • 操作符：主要包含四类操作符：子类型关系操作符、等价关系操作符、推理操作符和变量引用操作符。
  • 规格组成：共有三部分
    • 前置条件：对于输入参数的限制，通过requires子句完成。
    • 后置条件：对于运行结果的限制，通过ensures子句完成。
    • 副作用影响要求：在执行过程中会修改对象的属性数据或者类的静态成员数据。

　　同时要对所有情况进行限定，所以存在正常行为和异常行为的规格，signals语句，确定异常行为情况下抛出异常。

  • 除了方法规格外，还有类型规格来对Java程序中定义的数据类型设计限制规则。课程中的类型规格主要涉及两类：
    • 不变式限制：规定在所有可见状态下都必须满足的特性，形式为invariant P，其中invariant为关键词，P为谓词。
    • 约束限制：规定前序可见状态和当前可见状态的关系的约束，形式为constraint P。

应用工具链

JML应用工具链也比较全面，以下为常见的几种：

  • OpenJML，使用JML编译器来编译含有JML的代码，可以用来检查JML 规范，如果代码没有满足相应的规格，则会抛出相应的异常。
  • SMT Solver 对于代码进行静态检查。
  • JMLunit 生成自动测试样例

第二部分：部署JMLUnitNG/JMLUnit，针对Graph接口的实现自动生成测试用例

　　由于可能openjml还不支持/forall和/exist的语句，所以可能graph中原本编写的jml规格代码不能使用。所以自己编写了一个简单的加法运算代码（模仿讨论区大佬写的），采用jmlunit生成自动测试代码，主要进行相应的边界测试。

public class test {
    /*@ public normal_behaviour
      @ ensures \result == lhs + rhs;
    */
    public static int add(int lhs, int rhs) {
        return lhs + rhs;
    }
    
    /*@ public normal_behaviour
          @ ensures \result == lhs / rhs;
        */
    public static int div(int lhs, int rhs) {
        return lhs / rhs;
    }
}

　　下载好openjml和jmlunitng的jar包以后，由于脚本文件总是不成功，所以最后并没有使用脚本文件，而是直接使用命令行运行,运行以下三条命令行进行编译。

java -jar jmlunitng.jar test.java
javac -cp jmlunitng.jar *.java
java -jar openjml.jar -rac test.java

　　以下命令进行检测

java -cp jmlunitng.jar test_JML_Test

　　检测结果：

[TestNG] Running:
  Command line suite
​
Passed: racEnabled()
Passed: constructor Demo()
Failed: static add(-2147483648, -2147483648)
Passed: static add(0, -2147483648)
Passed: static add(2147483647, -2147483648)
Passed: static add(-2147483648, 0)
Passed: static add(0, 0)
Passed: static add(2147483647, 0)
Passed: static add(-2147483648, 2147483647)
Passed: static add(0, 2147483647)
Failed: static add(2147483647, 2147483647)
Passed: static div(-2147483648, -2147483648)
Passed: static div(0, -2147483648)
Passed: static div(2147483647, -2147483648)
Failed: static div(-2147483648, 0)
Failed: static div(0, 0)
Failed: static div(2147483647, 0)
Passed: static div(-2147483648, 2147483647)
Passed: static div(0, 2147483647)
Passed: static div(2147483647, 2147483647)
​
===============================================
Command line suite
Total tests run: 20, Failures: 5, Skips: 0
===============================================

　　由此可见自动生成测试样例中主要是对于边界的测试，int类型的边界范围测试，空和null，测试结果中add函数两次出现fail的范围就是最大值和最小值的相加，结果会超出int的范围。测试结果中div除法函数出现fail的范围是除数为0的情况，不合法。

第三部分：按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构

　　第三单元的三次作业主要是围绕规格的设置展开，根据规格填写主要的类与方法，三次作业主要是对于两个容器的功能的复用和迭加，从对于简单的路径的操作到对于图的多次操作，数据结构基本功不扎实的本人甚至感觉是java上了一次数据结构还债课。

第一次作业

　　第一次作业相对而言比较简单，没有过多的处理，只需要简单的增加删除和查询，但是传统的采用遍历查找的方式会使得时间复杂度大大提升，因此需要用到复杂度较低的数据结构hashmap的存储结构进行存储，采用hash图的存储。

　　小bug：

　　hashmap的查询过程中涉及到了equals和hashcode的重写问题。对于hashmap中key的比较，第一步是先比较hashcode，查找到相同的hashcode之后，第二步是equals的比较。hashcode的是基于内存地址进行的比较，所以如果对于自定义类，对于两个内容相同的对象来说hashcode也是不同的，所以必须要重写hashcode和equals的函数。

第二次作业

　　第二次作业稍稍比第一次复杂了一些，但也只是对于图的常规操作和计算，连通和最短路径的计算，采用单源的dij和多源的floyd都是很好的算法。我采用了floyd算法，虽然算法复杂度达到o（n^3），但是只是在图结构变更的时候进行计算，并且可以计算出所有的结果，但是却大大减少了查询的复杂度。

　　第二次代码直接复用迭代第一次的代码，没有进行过多的改变，但是在第一次的基础上加上了图的静态数组存储的数据结构，进行图的操作，求解最短路径等。

第三次作业

　　第三次作业难度陡然升级，在运行时间有限的情况下，算法的时间复杂度显得更加重要，虽然我最后并没有学会大佬们的拆点法，而是用了对于加入的路径在加入图的时候进行提前处理的方法（类似讨论区wjy大佬的想法），但也并没有爆tle，活过了强测。

　　第三次代码仍然复用第二次的代码，在第二次代码的基础上增加了存储的图的种类，也就是增加了图的静态数组的种类，以满足最少票价和最少换乘的查询。

　　我只放了第三次作业的uml图片，因为他完全代表了我整个作业的架构，最后都是在一个类中所有方法的堆叠。

第三单元oo作业总结

　　但是我最后分析，自己的三次作业都是代码的堆叠，只是在一个类中不断增加所需要的功能，最终使得一个类十分臃肿，完成所有的功能，虽然也完成了所有的要求，但是架构方面其实并没有达到要求，架构并不好，我也会认真学习例程的架构方式，更加认真的了解优秀架构的美，并且在自己的代码中尽力实现。

　　小trick：

　　三次作业中都是以查询的指令数为主，增加和删除的指令较少，所以把时间复杂度平均到这些指令中，直接构建查询的动态图，在每一次运行图结构变更指令的时候，更新查询动态图，可以使得大部分的查询指令的时间复杂度降低，进行直接的查询即可，有效减少运行时间。所以即使在更新查询动态图的时候采用的是复杂度较高的floyd算法，对于整体的运行时间影响并不是很大。

　　在查询动态图的更新的问题上，在作业中我采取了暴力直接重构的方法来更新动态图，尤其是对于remove的指令，过程十分暴力，运行时间的代价也比较大。

第四部分：按照作业分析代码实现的bug和修复情况

　　　　在这三次作业中，都幸运的活过了强测，并没有被hack出bug。

第五部分：阐述对规格撰写和理解上的心得体会

　　这一单元主要是围绕规格来展开，规格可以说是一种思想，可以在编写代码之前对于方法的效果提前限定并且设计好，但是设计的又仅仅是方法的功能，而并不需要考虑细致的实现方法，不受具体的数据结构或者算法的干扰，可以在编写代码前对于方法的功能性进行较为完备的设计。

  1. 精确描述方法所完成的任务和功能。在编写代码前不受实现方法的影响，单纯的设计好方法的功能，有利于之后代码的编写和生成。
  2. 更有效的发现代码的错误和bug。不论是没有正确实现方法的功能或者是没有正确的使用方法。
  3. 在多人协作的情况下，完备的规格设计可以使得合作更加简单方便，其他合作者并不需要了解代码内部如何生成，只需要阅读代码的规格，就可以清楚这个方法的功能和数据要求。
  4. 个人感觉编写规格是比编写代码需要更多的思考，他可以从上方直接完成类和方法的功能定义，对于代码架构的完成和优化是十分有帮助的。JML 将延迟过程设想的面向对象原则扩展到了方法设计阶段。

在讨论区大佬的带领下，在这一单元感觉也学到了不少有用的东西。

  1. maven文件的构建和使用，可以直接添加对于库的依赖，并且在库的内容改变的情况下，使用简单的git pull解决问题，在有多个文件依赖的情况下，是十分有效简单的。
  2. junit的测试框架生成，直接根据方法生成对应的测试方法，但是仅仅是简单的生成了相对应的测试框架，没有测试数据，其中的测试方法仍然需要自己填写，使用Assert断言进行结果的对比测试。
public class MyPathContainerTest {
    private final PathContainer pathContainer = new MyPathContainer();
    private Path path1, path2,path3;
​
    @Before
    public void before() {
        path1 = new MyPath(1, 2, 3, 4);
        path2 = new MyPath(2, 3, 4, 5);
        path3 = new MyPath(2, 3, 4, 6);
    }
​
    @After
    public void after() {
        // do something here
    }
​
    @Test
    public void testAddPath() throws Exception {
        Assert.assertEquals(1, pathContainer.addPath(path1));
        Assert.assertEquals(2, pathContainer.addPath(path2));
        Assert.assertEquals(3, pathContainer.addPath(path3));
        Assert.assertEquals(5, pathContainer.getDistinctNodeCount());
        Assert.assertTrue(!pathContainer.containsPathId(3));
        Assert.assertEquals(1, pathContainer.size());
    }
}

　　结果运行assert断言出现报错，即可确定代码中可能出现的错误。（由于自己的代码没有明显的错误，所以自己举得例子中是把前面expect写成错误的，但为了检测代码错误时候，expect的应当是正确答案）

java.lang.AssertionError: 
Expected :5
Actual   :6

 

 

相关推荐