OO第三单元总结

标签：person   类型   进入   man   expect   inf   lse   ora   sign   

1.梳理JML语言的理论基础、应用工具链情况

JML简介：

JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言(Behavior Interface Specification Language, BISL)，基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。

The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules. It combines the design by contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus.

使用 JML 来说明性地描述所希望的类和方法的行为，可以显著地改善整个开发过程。

JML表达式：

JML工具链：

• OpenJML，静态检查器，对JML语法进行检查

• JMLUnit，可以基于JML注释的java文件生成JUnit测试

• SMTSolver，在逻辑层面、对代码实现形式化验证。

2.部署JMLUnitNG/JMLUnit，针对Group接口的实现自动生成测试用例，并结合规格对生成的测试用例和数据进行简要分析

尝试了跑各种样子的MyGroup，虽然解决了目录和类间调用等等一大堆报错，但还有一些报错不知道怎么解决，比如下面这个：

最后写了个简单样例：

package test;
?
public class MyGroup {
?
        /*@ public instance model non_null int id;
      @ public instance model non_null int[] people;
      @*/
?
    private int[] people_;
    private int id_;
?
    public MyGroup(int id) {
        people_ = new int[100];
        id_ = id;
    }
?
    //@ ensures \result == id;
    public /*@pure@*/ int getId() {
        return id_;
    }
?
    /*@ also
  @ public normal_behavior
  @ requires obj != null && obj instanceof MyGroup;
  @ assignable \nothing;
  @ ensures \result == (((MyGroup) obj).getId() == id);
  @ also
  @ public normal_behavior
?
  @ requires obj == null || !(obj instanceof MyGroup);
  @ assignable \nothing;
  @ ensures \result == false;
  @*/
    public /*@pure@*/ boolean equals(Object obj) {
        if (!(obj instanceof MyGroup)) {
            return false;
        }
        return (((MyGroup) obj).getId() == id_);
    }
}

结果如下：

结合我的简单样例和大佬们的正经样例，可以看出生成大部分是特殊情况/边界数据。虽然跑出来了，但不知道为什么constructor测试不通过？？？总之jmlunitng实在是一副多年没维护的样子，感觉实用性很小（逃

3.按照作业梳理自己的架构设计，特别分析自己的模型构建策略

第一次作业：类构造与jml相同，容器统一使用ArrayList，搜索算法使用dfs。

第二次作业：加入Group类，容器仍然用ArrayList（bug修复中已修改），搜索算法使用并查集。

第三次作业：增加Relationship类，用于处理minPath。容器增加HashMap。minpath使用bellman-ford算法，stronglinked用两次dfs，blocksum用并查集。

总体来说是按jml来设计架构。

4.按照作业分析代码实现的bug和修复情况

第一次作业：强测0分，出现了超时和bug，把isCircle从bfs改成并查集后过了。

第二次作业：还是强测中出现了超时和bug，十分难过:(

第一个超时原因是contains和getperson都是重复用的，全部改掉后过了四个点。

第二个超时原因是getPerson用ArrayList，在设计频繁查找的地方都增加了HashMap之后变成WA。

第一个bug是relationSum的JML理解错了。因为评测提示是expect 1 get 0，一直以为是isCircle并查集写错了，de了发现写的完全没错。之后，在github上发现了大佬的评测机（感谢大佬），自己修改了下，瞬间发现了bug……具体问题是没把自己和自己的关系算进去，而且算的不是group里的是所有人的sum。

第二个bug是忘了考虑<1111。

第三次作业：强测有bug，还没修复，但比起前两次的惨状还是有进步的。minpath用了Bellman-Ford。stronglinked用了dfs，有bug……

算法效率和JML细节方面都出现了严重问题，在debug过程中加深了对JML的理解。

5.阐述对规格撰写和理解上的心得体会

通过前两次作业，发现照着jml翻译绝对会出现严重问题。JML可以让代码编写看起来非常直接，但其实只起到严格规范的作用，性能和架构方面需要实现者自己深入思考。另外，录播视频里提到的架构问题我在作业过程中没有考虑过，现在来看Network类确实实现了太多功能，应该进行抽象和分解，例如把算法放在单独的类里。其实本单元难度比我想象的要低（虽然由于自己菜前两次作业还是崩了），因为基本没有涉及写JML，感觉助教的工作量更大QAQ 从实验来看，我在写JML和检查JML正确性方面能力还需要提升。

OO第三单元总结

标签：person   类型   进入   man   expect   inf   lse   ora   sign   

原文地址：https://www.cnblogs.com/aurelina333/p/12944112.html