BUAA_OO_2020_Unit3_Summary

概述

通过Unit3的学习，我了解到JML规格化设计语言的相关知识，初步掌握通过JUnit开展单元测试的方法，并通过实现一个人际关系网络巩固所学内容、提升算法能力。本博文从JML语言与工具链、SMT Solver规格验证、JMLUnit测试用例生成、架构设计分析、Bug与修复及心得体会六方面展开，总结在Unit3中的收获。

1. JML语言与工具链

1.1 JML语言的理论基础

  • 本人用幕布软件生成的思维导图对JML语言的理论知识框架作如下梳理：

    思维导图可清晰地反映JML语言所涉及到的知识点主干，既便于学习过程中整体框架的构建，又便于日后的自我检测（根据思维导图的各条目复述知识细节），个人认为对计算机这种重视逻辑的学科的学习大有裨益

  • 根据上述思维导图，对JML语言的知识细节进行展开

    • 表达式
      • 原子表达式
        • esult表达式
          • 类型与返回值一致，表示方法执行后的返回值
        • old(expr)表达式
          • 类型与expr的结果一致，表示expr在相应方法执行前的取值
          • 对于对象引用v，若在方法执行过程中未改变v指向的对象，则old(v)与v具有相同取值
        • ot_assigned(x,y,...)表达式
          • 类型为boolean，表示括号中的变量是否在方法执行过程中被赋值
        • ot_modified(x,y,...)表达式
          • 类型为boolean，表示括号中的变量在方法执行期间的取值未发生变化
        • onnullelements(container)表达式
          • 类型为boolean，表示container对象是否非null且存储的对象不会有null
        • ype(type)表达式
          • 表示类型type对应的类型（Class），如 ype(boolean)为Boolean.TYPE
        • ypeof(expr)表达式
          • 表示表达式返回expr对应的准确类型，如 ypeof(false)为Boolean.TYPE
      • 量化表达式
        • forall表达式
          • 类型为boolean，全称量词修饰的表达式，表示对于给定范围内的元素，是否每个元素都满足相应的约束
          • 形式：(for Element element; element的范围; 相关约束)
        • exists表达式
          • 类型为boolean，存在量词修饰的表达式，表示对于给定范围内的元素，是否存在某个元素满足相应的约束
          • 形式：(exists Element element; element的范围；相关约束)
        • sum表达式
          • 返回给定范围内表达式的和，类型为相应的表达式
          • 形式：(sum Element element; element的范围；表达式)
        • product表达式
          • 返回给定范围内表达式的积，类型为相应的表达式
          • 形式：(product Element element; element的范围；表达式)
        • max表达式
          • 返回给定范围内表达式的最大值，类型为相应的表达式
          • 形式：(max Element element; element的范围；表达式)
        • min表达式
          • 返回给定范围内表达式的最小值，类型为相应的表达式
          • 形式：(min Element element; element的范围；表达式)
        • um_of表达式
          • 返回指定变量中满足相应条件的取值个数，类型为整数
          • 形式：( um_of Element element; element的范围；相应条件)
      • 集合表达式
        • new JMLElementSet {Element element | element的范围及满足的约束}
          • JML规格中构造的局部的容器
      • 操作符
        • 子类型关系操作符（<:）
          • E1<:E2表示类型E1是类型E2的子类型
        • 等价关系操作符（<==> / <=!=>）
          • 记b_expr1与b_expr2均为布尔表达式
          • b_expr1<==>b_expr2表示当且仅当b_expr1为true时b_expr2为true，当且仅当b_expr1为false时b_expr2为true
          • b_expr1<=!=>b_expr2表示当且仅当b_expr1为true时b_expr2为false，当且仅当b_expr1为false时b_expr2为true
        • 推理操作符（==>）
          • 记b_expr1与b_expr2均为布尔表达式
          • b_expr1==>b_expr2表示当b_expr1为true时b_expr2为true，亦可写作b_expr2<==b_expr1
        • 变量引用操作符（ othing / everything）
          • othing表示一个空集
          • everything表示一个全集
    • 方法规格
      • 场景
        • 正常行为规格（normal_behavior）
        • 异常行为规格（exceptional_behavior）
      • 条件
        • 前置条件（requires）
          • require P子句表示要求调用者确保P为真
        • 副作用（assignable / modifiable）
          • 表示方法在执行过程中会修改对象的属性数据或者类的静态成员数据
          • 可不指明具体的变量，而是用JML关键词来概括；亦可指明具体的变量列表
        • 后置条件（ensures）
          • ensure P子句表示要求方法实现者确保方法执行返回结果一定满足谓词P的要求
      • 常用关键字 / 子句
        • pure关键字
          • 表示方法无需描述前置条件，也不会有任何副作用
        • also关键字
          • 表示除了正常功能规格外，还有一个异常功能规格
        • signals子句
          • 记b_expr为布尔表达式
          • 形式：signals (***Exception e) b_expr
          • 表示当b_expr为true时方法会跑出括号中给出的相应异常
          • 简化的signals_only子句
            • 形式：signals_only (***Exception e)
            • 不强调对象状态条件，强调满足前置条件时抛出相应的异常
    • 类型规格
      • 不变式限制（invariant）
        • invariant P表示在所有可见状态下都必须满足谓词P
        • 只针对当前可见状态的取值
      • 约束限制（constraints）
        • 对前序课件状态和当前可见状态的关系进行约束
    • 父子类关系
      • 子类的不变式与父类的不变式（子类更严格）
        • I_Sub(c) ==> I_Super(c)
        • I_Super(c) =!=> I_Sub(c)
      • 子类重写方法的前置条件与父类方法的前置条件（子类更宽松）
        • Requires(Super::f) ==> Requires(Sub::f)
        • Requires(Sub::f) =!=> Requires(Super::f)
      • 子类重写方法的后置条件与父类方法的后置条件（子类更严格）
        • Ensures(Sub::f) ==> Ensures(Super::f)
        • Ensures(Super::f) =!=> Ensures(Sub::f)

1.2 工具链

  • 利用openJML和JMLUnitNG测试代码与规格符合的情况

    • 实测发现此类工具链尚不完善，故在作业的完成过程中较少加以应用，具体的实例分析见博客2 / 3两部分

  • 利用JUnit开展单元测试

    • JUnit单元测试在IDEA中即可展开，是一种方便高效的测试手段

    • JUnit单元测试的缺点在于仅能验证程序实现者书写的代码及使用的算法符不符合其所理解的规格，而不能测试程序实现者对规格设计者设计的规格是否理解到位

    • 以第三次作业中的queryStrongLink方法为例，展现JUnit单元测试所用代码（省略import部分及其他方法的测试）：

      public class MyNetworkTest {
    public MyNetwork network = new MyNetwork();

    @Before
    public void create() throws EqualPersonIdException, PersonIdNotFoundException, EqualRelationException {
        network.addPerson(new MyPerson(1, "aaa", BigInteger.ONE, 10));
        network.addPerson(new MyPerson(2, "aaa", BigInteger.ONE, 10));
        network.addPerson(new MyPerson(3, "aaa", BigInteger.ONE, 10));
        network.addPerson(new MyPerson(4, "aaa", BigInteger.ONE, 10));
        network.addPerson(new MyPerson(5, "aaa", BigInteger.ONE, 10));
        network.addPerson(new MyPerson(6, "aaa", BigInteger.ONE, 10));
        network.addPerson(new MyPerson(7, "aaa", BigInteger.ONE, 10));
        network.addRelation(1,2,1);
        network.addRelation(2,4,1);
        network.addRelation(3,4,1);
        network.addRelation(1,3,1);
        network.addRelation(7,5,1);
        network.addRelation(1,5,1);
        network.addRelation(5,6,1);
        network.addRelation(6,7,1);
    }
    
    @Test
    public void queryStrongLinked() throws PersonIdNotFoundException, EqualRelationException, EqualPersonIdException {
        ArrayList<Integer> list1 = new ArrayList<>();
        list1.add(1);
        list1.add(2);
        list1.add(3);
        list1.add(4);
        ArrayList<Integer> list2 = new ArrayList<>();
        list2.add(5);
        list2.add(6);
        list2.add(7);
        for (int i: list1) {
            for (int j: list2) {
                assertFalse(network.queryStrongLinked(i,j));
                assertFalse(network.queryStrongLinked(j,i));
            }
        }
        for (int i: list1) {
            for (int j: list1) {
                assertTrue(network.queryStrongLinked(i,j));
                assertTrue(network.queryStrongLinked(j,i));
            }
        }
        for (int j: list2) {
            for (int i: list2) {
                assertTrue(network.queryStrongLinked(i,j));
                assertTrue(network.queryStrongLinked(j,i));
            }
        }
        network.addRelation(1,7,10);
        list1.remove(0);
        for (int i: list1) {
            assertTrue(network.queryStrongLinked(i,1));
            assertTrue(network.queryStrongLinked(1,i));
        }
        for (int i: list2) {
            assertTrue(network.queryStrongLinked(i,1));
            assertTrue(network.queryStrongLinked(1,i));
        }
        for (int i: list1) {
            for (int j: list2) {
                System.out.println(i + ", " + j);
                assertFalse(network.queryStrongLinked(i,j));
            }
        }
        network.addPerson(new MyPerson(8, "aaa", BigInteger.ONE, 10));
        assertFalse(network.queryStrongLinked(1,8));
    }
}

2. SMT Solver规格验证

  • 目录树如下：

    其中，testOpenJML目录下仅有一个文件：Person.java，初步测试（静态测试）时其内容如下：

    
import java.math.BigInteger;

public interface Person extends Comparable<Person> {

    /*@ public instance model non_null int id;
      @ public instance model non_null String name;
      @ public instance model non_null BigInteger character;
      @ public instance model non_null int age;
      @ public instance model non_null Person[] acquaintance;
      @ public instance model non_null int[] value;
      @*/

    //@ assign 
esult == id;
    public /*@pure@*/ int getId();

    //@ ensures 
esult.equals(name);
    public /*@pure@*/ String getName();

    //@ ensures 
esult.equals(character);
    public /*@pure@*/ BigInteger getCharacter();
}

  • openJML

    利用WSL执行相关命令：

    最终得到的ret.txt中会出现一大堆混乱的报错信息：

    检查jdk版本为1.8，应该不存在问题，猜测是ubuntu运行环境不适用，故换用cmd执行Windows命令行操作，并保证jdk版本为1.8，仍出现类似的现象

    尝试许久后，仍未找出配置上的问题，故尝试用网页版的openJML接口，直接对课程组下发的第一次作业的Person.java规格进行静态测试，可以成功运行：

    正确时：

    错误时：

    （网页版JML网址：https://www.rise4fun.com/OpenJMLESC/）

    网页版JML的运行时测试会出现一系列问题，故不推荐

  • JMLUnitNG

    JMLUnitNG亦能对规格进行静态测试，并对实现代码进行运行时测试

    利用上述的Person.java，在WSL Shell中执行命令java -jar jmlunitng.jar ./testOpenJML/Person.java > ret1.txt后，ret1.txt与Shell界面上均无内容

    更改上述的Person.java中，让某一处出现不正确的规格语句"assign esult == id"，并再次执行上述命令，ret1.txt中仍无内容，而Shell界面上出现报错：

    由此可见，JMLUnitNG成功检测到规格中的错误，并向stderr输出报错信息

3. JMLUnit测试用例生成

4. 架构设计分析

4.1 第一次作业

UML类图

架构简述

  • 主要类：MyPerson、MyNetwork
    • MyPerson类以人的基本信息为属性，实现修改、返回这些信息的方法
    • MyNetwork类维护网络内人的数组，实现与人际关系网络中的用户功能相关的方法
  • 整体模型：邻接表存储的无向图模型
    • 本次作业内容较为简单，架构设计基本遵照课程组给定的规格
    • 根据UML类图，MyPerson与MyNetWork类分别实现Person与Network接口，并且两类与Network接口均存在1-*聚合关系
    • 涉及到的图的问题
      • 连通性判断（isCircle方法）

算法与性能

  • 本次作业在算法上无任何难点，唯一的在实现上有自由空间的方法是isCircle
  • isCircle采取BFS算法，时间复杂度为O(n+m)

4.2 第二次作业

UML类图

架构简述

  • 主要类：MyPerson、MyNetwork、MyGroup、UnionFindMap
    • MyPerson类与MyNetwork类的相关说明同第一次作业
    • MyGroup类维护群体内人的数组，设置一些记忆变量属性，实现与群体中信息的修改、返回相关的方法
    • UnionFindMap类构建并查集并实现有关算法，通过单例模式构造其单例作为MyNetwork类的属性
  • 整体模型：邻接表存储的无向图模型
    • 本次作业的架构设计在课程组给定的规格基础上，增加记忆变量与并查集
    • 根据UML类图，MyPerson、MyGroup与UnionFindMap类均聚合于MyNetwork类，由此可见MyNetwork类在人际关系网络中的“领导”作用
    • 涉及到的图的问题
      • 同第一次作业，连通性判断（isCircle方法）
      • 连通分量的维护（并查集的设计）

算法与性能

  • 本次作业对性能提出一定的要求，根据指导书上标程复杂度的提示，将所有方法的复杂度控制在O(n)量级以内是保证安全的
  • 为提高查找效率，本次作业中引入许多HashMap，通过哈希查找的机制使部分环节由原来的O(n)复杂度降为接近O(1)的复杂度
  • 更改第一次作业中isCircle的算法为并查集算法，所构造的并查集采取平衡多元树的数据结构，基本思想为将无向图中的各连通分量用若干棵平衡多元树表示，判断两个不同的顶点是否属于同一连通分量，仅需判断二者所在的平衡多元树的根节点是否相同即可
  • 在MyGroup中设ageSum（群体内人的年龄和）、ageSquareSum（群体内人的年龄平方和）、conflictSum（群体内character-conflict累计值）、relationSum（群体内link数累计值）、valueSum（群体内所有边的权值和）四个记忆变量，降低相关方法的复杂度
  • 部分方法的复杂度
    • MyNetwork类中的addRelation方法：使用并查集后由O(1)升至O(log(n))，但考虑到O(log(n))仍是一个较低的复杂度且可将MyNetwork中的O(n+m)（完全图情况下视为O(n^2)）复杂度降为O(log(n))，即消灭“超越瓶颈者”，故这种做法是值得的
    • MyNetwork类中的isCircle方法：O(log(n))
    • MyGroup类中的addPerson方法：O(min(n1, n2))，n1为群体内的现有人数，n2为所加入的人的邻接顶点数
    • MyGroup类中的getAgeMean、getAgeVar、getRelationSum、getValueSum及getConflictSum方法：记忆化后均由O(n)降为O(1)

4.3 第三次作业

UML类图

架构简述

  • 主要类：MyPerson、MyNetwork、MyGroup、UnionFindMap
    • 各类的相关说明同第二次作业
  • 辅助类：IdTuple、DisTuple
    • IdTuple：两个id构成的二元组，设相应的返回方法
    • DisTuple：一个dis(value)与一个id构成的二元组，设相应的返回方法
  • 整体模型：邻接表存储的无向图模型
    • 本次作业的架构设计在前两次作业及课程组给定的规格基础上，增加两个辅助类方便后续算法的实现(IdTuple可用Pair数据类型代替)，并在MyNetwork类中增加堆优化的Dijkstra算法与Tarjan算法的实现部分
    • 在实现Dijkstra算法及Tarjan算法后，MyNetwork类的代码略显臃肿，故可以将这两类算法所涉及的代码及属性抽象出来，用单独的两个类封装并与MyNetwork类交互，这样不但能够提升代码的美观程度，更重要的是能够提升代码的可扩展性，方便后续算法的更改
    • 对于较大型算法实现的相关类，可放在一个单独的package下；对于轻量级的辅助数据结构类，亦可放在另一个单独的package下
    • 与第二次作业相似，其他各类均聚合于MyNetwork类，MyNetwork类“领导”其余各类“各司其职”，很好地呈现出高内聚低耦合的效果
    • 涉及到的图的问题
      • 同前两次作业，连通性判断（isCircle方法）、连通分量的维护（并查集的设计与queryBlockSum方法）
      • 最短路径问题（queryMinPath方法）
      • 点双连通分量问题（queryStrongLinked方法）

算法与性能

  • 本次算法仍然在性能上有一定的要求，除queryStrongLink方法由于最多仅测试20条而可以降低复杂度门槛外，其余各方法均应将复杂度尽量控制在O(mlogn)量级内（指令数≤3000的限制保证O(mlogn)的复杂度足够安全）
  • 对于queryBlockSum方法，初看其规格，是一个O(n^3)形式的描述，在这种情况下应当自然地将抽象的规格语言转换为具体的问题，并在实际代码中用复杂度合理的算法去实现它，而非对着规格生搬硬套（正如同高考数学的圆锥曲线大题，若机械化地按照题目的描述去解决它，在颇为有限的考试时间内是不切实际的，故应将其转换为简单的模型求解）
    • 通过分析规格描述的逻辑并在草稿纸上进行简单的勾画，可知该方法要让我们实现的不过是统计无向图中的连通分量数，而第二次作业中引入的并查集就是一个天然的连通分量分割模型，故可直接在UnionFindMap中设表征连通分量数的记忆变量属性，在向网络中添加人或关系的时候对该变量进行更新
  • 对于queryMinPath方法，采用堆优化的Dijkstra算法，该算法在大二秋季学期的高工数据结构中作为重点学过，故在此不多赘述，可以使用java内置的优先队列PriorityQueue（底层基于小顶堆实现）来完成堆优化而不必手写堆（找到结果直接返回，可加入结果记忆变量进行改进，在每次有新的关系加入后更新该记忆变量）
  • 对于queryStrongLinked方法，有两种思路，一是暴力遍历法，二是tarjan算法，本人在这次作业中采用tarjan算法以有效降低方法复杂度，该算法的实现用到栈和递归的思想及做标记的手段，可有效地识别割点并在无向图的一连通分量中分出点双连通分量，若两顶点属于同一点双连通分量且该点双连通分量的顶点数≥3，则对于这两顶点的queryStrongLink判断为真（找到结果直接返回）
  • 新加入的部分方法的复杂度
    • MyNetwork类中的queryBlockSum方法：O(1)
    • MyNetwork类中的queryMinPath方法：O(mlogn)
    • MyNetwork类中的queryStrongLinked方法：O(n+m)

5. Bug与修复

5.1 第一次作业

  • 本次作业在中测、强测、互测中均为发现本人的Bug
  • 由于本次作业难度较低，在课下仅花费一小时左右的时间便顺利地完成，此后也没有发现什么Bug
  • 本次作业在互测中未发现他人的Bug

5.2 第二次作业

  • 本次作业在中测、强测、互测中均未发现本人的Bug
  • 本次作业在课下测试中同样没有发现什么Bug，完成过程较为顺利
  • 本次作业在互测中发现他人的多个Bug
    • 一名同学未认真阅读规格提示，计算平均值方差时不考虑除以0的情况；同时，这名同学未做好记忆化，导致getValueSum方法中出现双重循环，在互测中被极端图hack出ctle错误
    • 一名同学未理解清楚规格中各前置条件的逻辑划分关系，在实现addRelation方法时，遇到id1 == id2的情况直接return，而未考虑id1所表示的人是否在人际关系网络中
    • 一名同学在实现并查集的时候，部分情况下对根节点的判断不准确，反映出该同学对算法测试的全面度有所欠缺

5.3 第三次作业

  • 本次作业在中测、强测、互测中均未发现本人的Bug
  • 本次作业在课下测试中发现一个Bug，在与同学对拍结果的过程中发现，通过JUnit构建能复现错误的尽可能小的样例，并通过断点调试发现代码中的问题在于实现tarjan算法的过程中一处更新low值的地方传入的value值不正确
  • 本次作业在互测中发现他人的一个Bug
    • 一名同学在利用基于dfs的枚举判断双连通分量时，有时会将仅仅是强连通而非双连通的图判定为双连通，原因在于未将出发点加入visited集合中，体现出测试上的疏忽

6. 心得体会

  • 站在规格设计者的角度上，规格撰写是决定团队工程项目成败的关键，若规格撰写有失偏颇，程序实现者所书写的程序亦会出现问题。而规格撰写并非是一件容易的事。本人认为若要写出正确严谨的规格，需要从以下几大方面逐一考虑：

    1. 在一个类中，是否有始终不变的量（invariant）？是否有每次变化具有相同规律的量（constraint）？
    2. 对于一个方法，可能有哪些前置情况？是否存在交叉重叠（杜绝规格中出现此现象）？对应的是正常还是异常（normal_behavior / exception_behavior）？所对应的返回值及造成的后果何如？
    3. 对于已撰写的方法规格，语义是否清晰而简练（尽量避免规格过长以造成实现者的负担）？后置条件是否完整而能够避免不必要的多义性？最好能够仅从规格单方面切入，推导一下规格对应的具象需求是否如心里所想？
    4. 一个类若继承至另一个类，子类重写方法的前、后置条件与父类相应方法的前、后置条件及子类不变式与父类不变式是否满足应有的约束关系？

    总而言之，只有保证类规格与方法规格双方面的各分支要点正确，才可保证总规格正确。规格撰写是一个长期的过程，规格设计者在这一过程中难免会遇到许多坑，把自己遇到的坑积累记录下来，不定期的翻阅并警示自己下次不要犯类似的错误，久而久之正确性自然会提升。

  • 站在程序实现者的角度上，以本人完成这一次作业为例，相较于第一单元多项式求导及第二单元电梯而言，本单元可谓是轻松舒畅许多。其中很大一部分原因在于助教将工程的大体结构框架基本给定，规格撰写也特别详细，而且各函数划分很细致，方法规格上不存在“长篇大论”，大大减轻了同学们规格阅读的负担。需要注意以下几点：

    • 规格的重点是给出实现的前提与所应达到的效果而非实现的过程。在通过阅读规格对实现的前提与效果做到心中有数后，不能刻板地照着规格书写代码，而应该尽可能寻求能保持代码良好可读性及合适复杂度的方式完成实现。
    • 在规格出现明显的逻辑问题时，应尽可能迅速地同规格设计者联系，尽量避免自行更改规格，因为规格设计者是框架的给出者，在初期往往比程序实现者对工程具有更整体化的认识。正如第一次作业中有一个方法出现前置条件交叉重叠的问题，同学们第一时间向撰写规格的助教反馈，助教立刻修改规格，保证同学们代码实现的顺利进行。
    • 开展单元测试的过程中，对于任一给定规格的方法，尽可能根据规格中不同的前置条件展开充分测试，并通过repOK验证方法执行结束时各后置条件是否满足。换言之，测试应该尊重规格。

  • 有一个富豪（用户），雇了顶级的私人营养师（规格设计者）和厨师（程序实现者）。每天，厨师都会从营养师手中取过注明烹饪方式的当日食谱（规格），照着食谱采购食材（属性），并按照食谱上注明的烹饪方式（方法规格）制作大餐（完整代码）。有一天，富豪嗓子发炎了，由于营养师大意忘了这件事，仍然安排了油炸虾仁，结果导致富豪的嗓子更难受（规格设计未契合用户需求）。过了几天，轮到了厨师马虎，在做糖醋排骨的时候把盐巴当成白糖，结果做出了盐醋排骨，让富豪吃了很不高兴（程序实现未遵从规格）。富豪一气之下，将营养师和厨师都解雇了。

    • 上述故事性解读或许不大贴切，但体现出软件项目中规格设计与程序实现的过程相分离、规格设计者与程序实现者协作配合的过程，阐释了这样一个道理：规格设计者与程序实现者任何一方的大意都有可能造成软件项目的失败。
    • 规格的给出能够提高代码实现的条理性和效率，同时在很大程度上避免了二义性，让设计更加明确化。其实在完成电梯作业时，我就考虑过是否有必要引入一个类似“规格”的东西。因为对于我所书写的一个融合上升一层和开关门的方法，由于实现时所遵照的流程和后续调用时所认为的流程不一致，导致出现些许不合理调用的现象，也就是前后的逻辑“打架”。这时，我立刻用英文为该方法的流程约束做了说明，但这仅仅只能作为我个人在编程过程中的提示，而无法达到逻辑上的完备。而第三单元的规格正好是一种逻辑上的约束，是避免我上述所说问题出现的一有效手段。
    • JML规格在网上的资料较少，或许在实际工程项目中有更为高效的规格实现手段，但本人认为本单元学习关注的核心不应是JML的知识体系本身，而应是契约式编程的思想与魅力。尽管本人认为本单元在作业设计上还存在提升空间，例如工程框架给定过于具体、未训练继承中的规格关系这一知识点等，但仍要感谢课程组的辛勤付出，无论是从规格撰写及修正、评测数据设计还是实验环境维护上均花了不少心思，同时也希望下一届的学弟学妹们能够在本单元中有更多收获！
【推广】 免费学中医，健康全家人
原文地址：https://www.cnblogs.com/palemodel/p/12934693.html