OO第三单元总结

Posted 2020-11-30 hydride

1 JML语言的理论基础及应用工具链

1.1 JML语言

Java建模语言(JML)是一种行为接口规范语言，可用于指定Java模块的行为。它结合了Eiffel的“契约设计(design by contract)”方法和Larch系列接口规范语言的基于模型的规范方法，以及细化演算的一些元素。对JML语言起到理论支撑作用的文章主要是以下三篇：

• Leavens G T, Cheon Y. Design by Contract with JML[J]. 2006. 这篇文章解释了JML语言作为一种契约设计语言的基本使用方法；
• Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll. Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. In Formal Methods for Components and Objects (FMCO) 2005, Revised Lectures, pages 342-363. Volume 4111 of Lecture Notes in Computer Science, Springer Verlag, 2006. 这篇文章包含对JML语言的解释以及对主流工具的介绍；
• Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer, 7(3):212-232, June 2005. 该文章列举了当前所有已知的JML工具并相应地进行了简单介绍。

1.2 JML语言相关工具

现在已经有大量的开源和非开源的基于JML语言编写的相关工具。其中，应用相对广泛的主流工具有如下几个：

• The AspectJML tool：为Java和AspectJ做运行时检查的工具
• The jml4c tool：基于Eclipse Java编译器开发的JML语言编译器
• Sireum/Kiasan for Java：一个基于契约的自动化验证测试工具
• JMLEclipse：在Eclipse的JDT编译器基础上开发的JML工具包
• JMLUnitNG：自动化测试生成工具
• JMLOK：用随机测试检查java代码是否符合JML规格并对不一致现象给出可能的原因

2 部署JMLUnitNG并进行简要分析

JMLUnitNG是一个自动化的单元测试用例生成工具，专门为JML语言标注的Java代码而设计的。理论上，可以基于代码的JML注释来生成较为完备的测试用例。但正如讨论区里某些同学指出的，该工具并不支持JML语言中forall和exist等语法，因而对于本单元程序的帮助极为有限。下面我只对一个演示用程序做了简单的JMLUnitNG实践，更多的对于该工具的使用还有待进一步探索。

测试代码：

// demo/Demo.java
package demo;

public class Demo {
    /*@ public normal_behaviour
      @ ensures 
esult == lhs - rhs;
    */
    public static int compare(int lhs, int rhs) {
        return lhs - rhs;
    }

    public static void main(String[] args) {
        compare(114514,1919810);
    }
}

3 架构设计及bug分析

3.1 第1次作业

事实上第1次作业并没有太多和架构有关的内容，它的主要目的是帮助大家熟悉JML语言并根据JML方法规格正确地写出相应的Java代码，方法的规格逻辑也都比较简单，无需复杂的架构设计。主要是实现了MainClass，MyPerson和MyNetwork类即可完成任务，代码量和难度不是很大。

仅用了几个小时的时间就完成了程序并通过中测，但是由于没有好好利用JUnit进行测试，仍然停留在前两个单元那种过了中测，强测也就差不多了的心态，导致强测的时候损失惨重。虽然debug的时候发现都是一些很小的bug但是依然造成了不可弥补的损失。这让我认识到测试之于编程的重要性。

3.2 第2次作业

第2次作业中，新增了Group接口，于是新构建了MyGroup接口用于给关系网里的人分组。代码在逻辑上的复杂程度也不是很高，但是麻烦的点还是在于构造测试数据上面。我个人能力有限构造了几百个测试数据以及使用Junit进行了测试，但是最后居然在某个“元素数量小于1111”的条件上面跪了。。确实是自己在测试的时候并没有构造那么多的数据，而且由于手动构造数据和个人能力的限制，对于算法的时间复杂度优化我并没有做太多的考虑，也导致了一些失分。

 

3.3 第3次作业

第三次作业比前两次增加了Network中的几个成员方法。主要难点在于设计了点双连通和最短路的算法。我个人在算法设计的时候凭借去年数据结构所学的图算法按照自己的理解和记忆利用迪杰斯特拉和BFS的思路写了两个算法。通过了中测，但是在强测的时候又又遇到了时间的问题，导致了部分失分。

 

4 心得体会

这一单元的训练重点，我认为，在于对于JML规格的理解以及将JML规格正确且高效地转化为Java代码的能力。而通过这一单元的三次作业，我相信我已经很好地掌握了这些能力。JML规格，正如老师在课上提到过的，确实是一种很好的工具来显式地表达程序员在设计架构和定义方法功能时的思路。

另外，我个人感觉我通过第一次作业已经比较熟练的掌握了读JML的方法了，后两次作业拼的基本上是测试的全面和算法的优越性了。但是三次作业过后，我在JML书写上面只停留在实验课的那二十多个填空上。而且那还是刚学，所以填写的效果也不是很好。总而言之，对于一个菜鸡来说，我这一单元新掌握的本领实在是少，和大佬们之间的差距又变大了。（）所以希望以后有可能的话加一些JML语言书写的训练叭）

OO课从讨论区到讨论课都能看出老师和助教们的认真负责，和大佬同学们的无私奉献，希望OO课越来越好！也希望我们的学弟学妹能够学到更多，不要像学长我一样菜。