第三单元总结

关于JML语法

书面定义：JML (Java Modeling Language) 是用于对 Java 程序进行规格化设计的一种表示语言，是一种行为接口规格语言。

个人理解：

• 设计文档接口，限定输入输出，一个很直观的例子就是本单元大部分指导书都在JML的代码里，不像前两个单元需要做许多的书面定义。

• 本单元着重训练了面对设计好的JML规格进行开发，其次也训练了依据JML规格设计测试数据。

• 虽然很熟悉，但几乎没有亲自动手写JML的代码。

• 有时一行JML可能需要上百行代码来实现（要求高复杂度或辅助方法甚至类）

• 有时是几行JML也可能只需要一行循环（包含很多\old描述）

• 并无完善的自动化测试工具，JUnit仅方便模块化测试，对JML无特殊支撑。

如何“翻译”JML

• 大部分规格都可以一一对应代码语句。
• 少部分语句需要仔细设计各个类额外的方法，甚至辅助类。
• “直译”未必行得通，需要考虑复杂度与边缘数据。

如何选择容器与数据结构

根据操作容器的方法特点选择容器，如

 @ public instance model non_null Person[] acquaintance;
 @ public instance model non_null int[] value;

对应的方法其中有

    /*@ public normal_behavior
      @ requires (\exists int i; 0 <= i && i < acquaintance.length; 
      @          acquaintance[i].getId() == person.getId());
      @ assignable \nothing;
      @ ensures (\exists int i; 0 <= i && i < acquaintance.length; 
      @         acquaintance[i].getId() == person.getId() && \result == value[i]);
      @ also
      @ public normal_behavior
      @ requires (\forall int i; 0 <= i && i < acquaintance.length; 
      @          acquaintance[i].getId() != person.getId());
      @ ensures \result == 0;
      @*/
    public /*@pure@*/ int queryValue(Person person);

• 当然可以选择两个List
• 但可以发现，由于这两个List的元素一一对应，且通常需要成对操作或根据acquaintance取value，因此可以使用Map合并两个List

根据数据规模选择数据结构，如

    /*@ ensures \result == (people.length == 0? 0 : ((\sum int i; 0 <= i && i < people.length; 
      @          (people[i].getAge() - getAgeMean()) * (people[i].getAge() - getAgeMean())) / 
      @           people.length));
      @*/
    public /*@pure@*/ int getAgeVar();

该方法返回组内成员age的方差，组内成员可以增加或删除

• 当然可以每次查询都重新计算（ O(n) ）
• 但考虑到人数范围[1,5000]，age范围[0,200]，因此可以选择在每次增删人时维护 AgeMean与AgeVar（ O(1) ）（AgeVar不直接维护，而是维护平方和，用公式计算，注意整除差异！）

架构设计

本单元自己需要设计的方法不多，大部分照着规格都能直接写出，仅梳理几个算法难点。

第一次作业

容器

• acquaintance[]与value[]合成 HashMap<Person, Integer>
• people用HashMap<Integer, Person> 表示

算法

• 判断是否联通以及联通块数，并查集路径压缩 O(1)

第二次作业

容器

• groups用HashMap<Integer, Group>
• messages用HashMap<Integer, Message>

算法

• 年龄方差、均值，在增删人时维护年龄和与年龄平方和O(1)，O(1)查询，公式计算方差时注意整除约分带来的影响。
• valueSum同样增删人时O(1)维护，O(1)查询（注意2倍），为了维护方便允许破坏类封闭性

第三次作业

容器

• emojis用HashMap<Integer, Integer>

算法

• 最短路径用dijkstra，具体实现来说用了priorityQueue，需要注意从队列中删除节点的时机（如在边界被多次更新最短距离的节点）。还有需要注意priorityQueue需要实现的比较器，有两个方案
  • 第一个，实时比较节点distance
  • 第二个，比较节点存入队列时的distance，需要建立辅助类保存距离，有同一节点多个距离的情况，需要及时清理。

关于测试

• 设计测试数据时可从容器与算法两方面考虑
  • 边缘数据，中间量是否爆int
  • 考虑算法复杂度，可针对维护与查询分别构造针对数据
• JUnit单元测试快捷好用
• 需根据JML与实现代码的复杂度相对大小设计测试代码
  • 有时JML很简洁，代码复杂度很高，此时对应JML来设计测试用例
  • 有时JML描述啰嗦，代码很短且结构清晰，此时先确认JML的语义实现完全再仅针对实现代码进行测试是最高效的。
• 本单元适合对拍而不是正确性解析

Bug分析

前两次作业没出现bug，但自己测试时需要注意异常情况下的id（重复id或emojiId）

最后一次作业由于没安排好时间周末下午才开始写，没时间测试了最后强测50，一共两个bug

• 一个是低级错误没看清JML，随机数据都能跑出来，挂了几个强点也因此挨了很多同质刀。
• 还有一个是dijkstra算法出了问题，priorityQueue的比较器只存了id，比较实时距离，我当成了比较存入距离进行了清理，强测最短路径的点出了问题。

心得体会

• JML虽然没有完善的自动化测试工具，但配合JUnit的单元测试的面向“接口”的测试数据构造更系统，也更全面。

• 规格理解并不难，难的是选择合适的容器、算法以适应不同的数据规模。

• JML有时可以简化描述，但有时不能很好地平衡JML的复杂性，会出现数十行JML语句仅单行循环表示的“反客为主” 的情况，这也是我认为契约式编程的一大缺点，在实际工程中或许可以通过在类似场景“直接描述代码“避免。

• 现在应该几乎是本学期最忙的时候之一，希望同学们留足测试时间，避免出现时间不够，低级错误导致大量失分的遗憾。

OO第三单元总结

原文：https://www.cnblogs.com/LNTisNotaTree/p/14825490.html