OO第三单元总结

Posted dengtc

tags:

篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了OO第三单元总结相关的知识,希望对你有一定的参考价值。

OO第三单元总结

前言

? 本单元中,初次接触到了The Java Modeling Language (JML)这种语言,主要尝试了根据规格进行相应代码实现,及根据代码或需求抽象出相应规格的练习。从PathContainer,Graph到RailwaySystem,一路发展过来,在实现这些接口的新方法时,都是按照方法规格进行了代码实现。同时,也尝试了通过规格来进行一定的形式化验证。

一、JML语言

(1)JML语言的理论基础

JML是一种形式化的、面向JAVA的行为接口规格语言

JML允许在规格中混合使用Java语法成分和JML引入的语法成分

JML使用Javadoc的注释方式

? ? 结构化、扩展性强

? ? 块注释:/@ … @/

? ? 行注释://@

JML语法

? Precondition

    ? /*@ requires P; @*/

? Postcondition

    ? /*@ ensures P; @*/ 

? Side-Effects

    ? /*@ assignable list;@*/

? Exception

    ? /*@ signal (Exception e) P;@*/

? Invariant

    ? /*@ invariant P; @*/ 

? Constraint

    ? /*@ constraint P; @*/ 

? method result reference

    ? \\result 

? Previous expression value

    ? \\old(E)

Using private fields in specifications

    private /*@ spec_public @*/ Type property; 

Fields not null

    Private /*@ not_null @*/ Type property;

Declare spec variable

    //@ public model Type x; 

Quantifiers

Iterating over all variables

    (\\forall T x; R(x); P(x)) 

Verifying if exist variables

    (\\exists T x; R(x); P(x)) 

Num of elements

    (\\num_of T x; R(x); P(x)) 

Sum of expression

    (\\sum T x; R(x); E)

方法规格抽象

? ? 执行前对输入的要求----前置条件(precondition)

? ? 执行后返回结果应该满足的约束----后置条件(postcondition)

数据规格抽象(类型抽象)

? ? 数据状态应该满足的要求----不变式(invariant)

? ? 数据状态变化应该满足的要求----约束(constraint)


(2)应用工具链

OpenJML

? OpenJML能够检查Java Modeling Language中使用规范注释的Java程序,并为JML的许多功能提供强大的支持。

? OpenJML中的验证可以通过使用我们的扩展静态检查工具或使用我们的运行时断言检查功能来执行。运行时断言检查通常更容易编写规范,而静态检查可以更好地保证程序行为。

? OpenJML不是定理证明器或模型检查器本身。OpenJML将JML规范转换为SMT-LIB格式,并将Java + JML程序隐含的证明问题传递给后端SMT求解器。与最流行的SMT解算器集成。

JMLUnitNG

? JMLUnitNG是一个用于JML注释的Java代码的自动化单元测试生成工具,包括使用Java 1.5+特性的代码,例如泛型,枚举类型和增强的for循环。与原始的JMLUnit一样,它使用JML断言作为测试oracles。它通过允许轻松定制要用于测试类的每个方法参数的数据,以及使用Java反射自动生成非基本类型的测试数据,改进了原始JMLUnit。

......


二、JMLUnitNG测试

测试Path接口实现

package demo;

import java.util.ArrayList;

public class Test {
    public ArrayList<Integer> nodes = new ArrayList<Integer>();

    /*@ public normal_behavior
      @ ensures \\result == nodes.size();
      @*/
    public /*@[email protected]*/ int size() {
        return nodes.size();
    }
    
    public static void main(String[] args) {
        Test t1 = new Test();
        t1.nodes.add(2);
        t1.nodes.add(1);
        t1.nodes.add(4);
        t1.nodes.add(7);
    }
}

技术图片

将测试代码放入demo文件夹

技术图片

完成测试


三、作业架构设计

第一次作业

技术图片

MyPath,用ArrayList存Path,用HashMap存点,实现了Path接口;

MyPathContainer用HashMap实现了pathid与path的相互查询、增添、删除,及不同节点的统计,实现了PathContainer接口。


第二次作业

技术图片

Solve类主要进行最短路计算,使用floyd算法,每当有path的增添和删除时,就重新算一遍,其中有HashMap分别存储节点邻接表,及最短路数值。

MyGraph实际上可以继承上一次作业的MyPathContainer。


第三次作业

技术图片

第三次作业架构确实不太理想,我把图计算相关四个方法的实现都写在了solve类里,成就了一个超级类,以至于,上边的图把方法展开,字都小的看不到了,这里就不放出来了。

本来想的是一个方法一个类,但由于工程量还有自身的一些原因,最后没有选择这样做,感觉自己每次写代码还不能做到从容不迫。

算法使用的spfa,用HashMap标记了已经算过的最小值,可以直接重用;每当有Path的增添、删除时,作为标记的HashMap清空。


四、Bug及修复

第一次作业

? 未被查出bug。

第二次作业

? 强测与互测,均有超时情况。使用floyd算法,常数过大。

? 修复:对于floyd算法三重循环嵌套的语句进行简化,即可满足性能要求。

第三次作业

? 互测,有超时情况。使用spfa算法,进行计算时,对于一个点,任何数据的更新,都把该点加入松弛队列当中,使得时间复杂度过高。

? 修复:未能在不更换算法的基础上修复bug。


五、心得体会

? 在本单元的学习中,随着对JML语言的熟悉,我逐渐认识到了规格化设计的优势。

? (1)抽象的思想,使得在考虑代码架构时,不必过早的扎入代码的具体实现中。同时,还能认识到对于类或方法抽象出的规格与需求间的联系。

? (2)在合作进行代码开发时,通过规格,对各个类、方法,进行一定的约束。如此,无论是提供者还是调用者,都能减少不必要的交流,通过规格进行高效的开发(我的代码满足规格即可)。

? (3)通过JML相关工具,可以进行规格与实现之间的验证,保证代码实现能满足规格要求。进行形式化验证,使出Bug几率大大降低。

? 除此之外,对于程序时间复杂度方面有了更多的认识。在三次作业中,第二次强测有超时,第三次互测有超时。让我意识到,规格并没有对时间维度进行限定,按照规格完成代码,大概率保证了正确性,但并不一定满足性能要求。我们还要在保证规格的约束下,尽可能的兼顾架构与性能,把代码写好、写漂亮。

以上是关于OO第三单元总结的主要内容,如果未能解决你的问题,请参考以下文章

oo第三单元总结

OO第三单元总结

OO第三单元总结

OO第三单元总结

OO第三单元总结

OO第三单元总结