码迷,mamicode.com
首页 > 其他好文 > 详细

OO第三单元总结

时间:2020-05-23 20:14:55      阅读:50      评论:0      收藏:0      [点我收藏+]

标签: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表达式:

表达式含义
\result 方法返回值
\old() 表示进入方法时刻某个数据的值
(\forall ; ; ) 全称量词
(\exists ; ; ) 存在量词
a==>b a推出b
\sum 给定范围内表达式的和
\num_of 指定变量中满足相应条件的取值个数

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

(0)
(0)
   
举报
评论 一句话评论(0
登录后才能评论!
© 2014 mamicode.com 版权所有  联系我们:gaon5@hotmail.com
迷上了代码!