BUAA OO 第三单元总结

Posted 2020-11-30 yszhao

目录

• Part 1 JML
  • 规格（specification）
  • JML
  • JML的规格变量
  • 不变式（invariant）和变化约束（constraint）
  • JML的方法规格
  • JML的表达式：
  • JML的工具链介绍
• Part 2 自动生成用例测试
  • JMLUnitNg自动生成用例测试
  • 定制化的自动生成用例测试
• Part 3 程序结构设计
• Part 4 Bug分析
• Part 5 心得体会

Part 1 JML

规格（specification）

规格既是一种描述，也是一种契约。一方面，规格描述了一个复杂的、具体的代码实现的行为逻辑。比如，使用HashMap的用户并不需要知道该类解决哈希冲撞的具体方法，也不需要知道这个类会不会使用红黑树。这极大地方便了使用者。另一方面，规格是调用者和被调用者之间的一种契约。我在第一单元作业中就出现过被调用的函数在出现问题时返回null而调用者忘记处理这种返回值而出错的情况。这种契约在代码量较少、工程较为简单时可能显得有些多余，但进行大型、复杂代码工程时，这种契约式不可或缺的。

JML

JML全称为Java Modeling Language，是一种严格的规格实现方式。另一种规格的实现方式是自然语言。JML相比于自然语言而言最大的优势是语言的严谨性。当然，这种严谨性的代价便是更加冗长、更加晦涩难懂的语言。

JML的规格变量

• 使用spec_public将不可见的属性声明为可见的规格变量：

  private /*@ spec_public @*/ ClassName attributeName;
  

• 使用model：

  //@ public model non_null int[] elements;
  //@ public static model non_null int[] elements;
  //@ public instance model non_null int[] elements;
  

  其中后两者区分了静态和实例两种规格变量。在interface中声明规格变量需要进行区分，而在class中一般不必。

不变式（invariant）和变化约束（constraint）

不变式和变化约束都是对规格变量的一种约束。两者的区别是，不变式强调变量的取值的空间，而变化约束强调变量在前后两次取值的过程中应遵守的约束。

不变式和变化约束都是针对可见状态而言的。它们允许在不可见状态下，变量不符合约束。通俗而言，不可见状态是指一个类中能够修改某个变量的方法在执行过程中该变量的状态。比如，在calculateDistance方法执行过程中，distance变量可以短暂地为负。当然，在方法执行完成后，相应变量就应当符合不变式和变化约束。

两种约束的格式如下：

//@ invariant Boolean_expression
//@ constraint Boolean_expression

JML的方法规格

一般而言，方法规格包括：前置条件、后置条件、副作用、异常处理等方面。JML的方法规格也是如此。一个常规的JML方法规格如下：

/*@
  @ public normal_behavior
  @ requires Boolean_expression;
  @ assignable 
othing (or something);
  @ ensures Boolean_expression;
  @ also
  @ public exceptional_behavior
  @ requires Boolean_exception;
  @ assignable 
othing (or something);
  @ signals (SomeException e) Boolean_expression;
  @ signal_only SomeException
  @*/

JML使用normal_behavior和exceptional_behavoir来进行异常分类处理，使用requires来表达前置条件，使用assignable来表达副作用，使用ensures来表达后置条件。

此外，方法规格还可以增加修饰符/*@ pure @*/，用来表示该方法没有前置条件，也没有副作用。使用pure修饰符修饰的方法可以被其它JML规格调用。

JML的表达式：

• 原子表达式：

  表达式	语义
  esult	方法的返回值
  old(expression)	某方法执行前表达式的取值
  ot_assigned(x,y,...)	表示方法执行过程中未被赋值的变量
  onnullelements(container)	表示集合中的元素非空
  ypeof(expression)	表达式返回值的类型

• 量化表达式：

  基本结构：( otation variable_declaration; Variable_constraints; expression)

  其中，notation包括：forall, exists, sum, product, max, min, num_of等。

• 集合表达式：

  基本结构：new ST {T x | P(x)}

• 操作符：

  包括子类关系操作符（<:）、等价关系操作符（<==> or <=!=>）、推理操作符（==>）和变量引用操作符（ othing or everything）。

JML的工具链介绍

JML的相关工具链包括：OpenJML, JMLUnitNg。OpenJML可以对JML进行语法检查，JMLUnitNg可以自动生生成测试数据。这两个工具，从目前的评价来看，普遍无法达到预期的测试效果。

Part 2 自动生成用例测试

JMLUnitNg自动生成用例测试

JMLUnitNg可以自动生成测试数据，这是一种进步。但是，它并不了解被测函数的具体意义，被测函数参数在具体语境下的含义，因此测试数据大多是一些边界数据。比如，在测试Group::equals方法时，它只会传入null，而不是构造的Person类。这大大限制了JMLUnitNg在实际场合中的应用。这也是语境无关测试的通病。

想要解决这一问题，一种策略便是事先给定测试输入的概率分布。比如，对于人的年龄，虽然程序中使用int32来表示这一数据，但显然，不会有人出现INT32MAX的年龄。我们可以给定一个数据的分布，比如，([0,200])的均匀分布。这种细化的测试更加符合实际场合。

除了输入数据分布的问题，输出验证也是一个非常关键的问题。我们可以用各种手段获得输入数据——无论是定制的数据生成器，还是在实际应用场合中采集数据。但是，将输入数据提供给程序后，如何验证输出的正确性，是所有自动化测试都需要面对的难题。而使得问题更加复杂的是，正确性的验证往往与程序本身密切相关，正确性验证的难易程度也取决于程序本身的性质。比如，一个通过哈希函数的输出值反解哈希函数的输入值的程序就非常容易验证；而像我们第二单元的电梯作业，验证起来就相对较麻烦，因为有很多的约束条件需要考虑。

定制化的自动生成用例测试

我在这一单元作业的测试中采用的是定制输入+对拍的方法。数据生成方面，我编写了相关生成程序，读入用户给定的指令分布（如下代码所示），生成相关随机化指令。验证方面，我主要与其他同学进行对拍。

{
	"seg_num": 2,
	"seg_1": {
		"name": "comment",
		"ag": 1,
		"ap": 1,
		// ...
	},
	"seg_2": {
		"name": "boot",
		"ag": 10,
		"ap": 800,
		"ar": 1000,
		"atg": 3000
	},
    // ...
}

在验证方面，除了不同代码实现人员之间可以进行对拍，自己的两种实现也可以实现对拍。这在程序算法优化方面有很大的用武之地。比如，在用暴力搜索算法实现点双连通的判断之后，可以再次基础上实现Tarjan算法，然后与原来的算法进行对拍。

Part 3 程序结构设计

在程序的大框架上，其实并没有什么设计的空间了。毕竟，课程组已经给出了相关接口，而我们所需要做的只是高效地实现这些接口。我在这三次作业中，基本也只是实现了这些接口，只是可能在一些细节方面进行少许的优化。比如，容器选择方面，Person类实现的acquaintance到value的对应关系，就可以使用HashMap来实现；Network类中，对所有人的money属性进行记录，便可以使用规定了初始空间大小的HashMap来实现（当然，也可以作为Person的一个属性进行管理，但考虑到Person类没有管理money的相关方法，因而也就没有存储到Person中了）。此外，本次作业还需要实现一些高效的算法，而不是使用最简单的暴力搜索方法。比如带有堆优化的Dijkstra算法、Tarjan算法、并查集算法等。

但是，从理论课上来看，这一单元的作业似乎是想让我们做一些设计的。比如，在理论课上，吴际老师提出了一种将节点进行聚类的思路。这可能是一种先进行图分割，再将整个图部署到不同节点的思路，虽然本次作业中完全可以不采用这种方法，但是这种思路在图的规模达到一定大小之后可能有比较高的效率。吴老师提出的另一种想法是以边为基本存储单元进行检索，虽然我没有想出这具体是一种什么样的思路。

Part 4 Bug分析

由于前期进行了几万条指令级别的对拍，所以在中测、强测、互测中都没有被找出bug。在第二次作业中，有一位同学使用了二重循环来计算Group中的关系总和valueSum，包括我在内的其他人纷纷构造类似数据进行hack。在其他的互测中，我也没有发现什么bug，可能是大家代码的质量普遍比较高。

Part 5 心得体会

1. 规格的思想在大型工程中有着很大的作用。对于一个人完成的工程，今天调用函数的你，可能会忘记十天前写函数的自己是怎么约定输入和返回值的。对于多人完成的工程，提前规定好接口，那更是十分重要了。

2. JML是一种实现规格的途径，但并不是很理想（这一部分可能只是对JML的抱怨，读者可以略过）：

   • JML的语言，为了严谨性而放弃了直白性、简洁性。写JML的人，需要将自己的想法、用户的需求表达成JML的形式，这个过程是容易出错的。读JML的人，需要通过冗长的描述理解写JML的人的意图，这也不是一件轻松的事。试读下面文字：

     Objective consideration of contemporary phenomena compels the conclusion that success or failure in competitive activities exhibits no tendency to be commensurate with innate capability, but that a considerable element of the unpredictable must invariably be taken into account.

     我在读JML的时候，虽然也能理解，但是总觉得JML把一些本来很直白的意思说得很晦涩，就像上面这段文字一样。

   • JML语言忽视了程序中的变量在具体应用场合的语境意。以用户的年龄为例，正常程序员都知道，人的年龄有一个区间范围（虽然大家对于这个具体数值可能有不同的观点），如果现要求两个用户的年龄之差，正常程序员也不会考虑会不会超过int32的表示范围。但是作为JML，它要么自行规定年龄的范围，要么让实现人员改用BigInteger。事实上，在程序编写的过程中，有许多常识性的知识，如果要JML逐一规定，必然非常麻烦。

     • 很多ML领域的从业者都知道im2col到底干了什么，但是用JML描述出来，写的人需要花很多时间，读的人也读的费劲。

   • JML语言缺乏完善的工具链，在工业界也没有被广泛采用。JML试图找到一种通用的设计、验证的固定方法，而这种忽略每一个项目具体应用场合的验证是很难的。另一方面，如果编程人员想要进行严格的验证，他完全可以使用别的专门为某个领域进行形式化验证而设计的编程语言。

   • JML不能给编程人员提供一个全局的、整体的描述。比如，指导书上会交代我们写的代码是用来干什么的，它的基本功能是什么；而JML做不到这一点。

   • 我个人认为，JML的一个合适的作用是与自然语言描述互相补充。就像绝大多数数学教材，不可能只有严谨的数学定义、定理、公式，还需要有自然语言来描述它们的意义。

3. 相比于用JML实现规格，我更愿意用自然语言来描述。

4. 如果不考虑同学之间进行对拍这种方式，JUnit也是一种很好的选择。

---

其他一些建议：

• 个人感觉一个单元的多线程练习并不是很足够，也许第三单元可以继续做多线程练习。
• 个人感觉我在这一单元并没有做多少规格化设计方面的练习，因为所有的规格都由课程组给出了。也许以后可以把规格让同学们自己实现。