第三单元JML规格总结

第三单元学习了JML规格描述语言,根据JML的规定编写对应的方法,同时也复习了数据结构的知识,并且也考察了程序的时间复杂度。

一.JML语言

 理论基础

  JML全名为Java Modeling Language(Java建模语言),在Java代码中增加一些不影响程序正常编译运行的符号用来标识一个方法是干什么的。通过使用JML,程序员能够描述一个方法的预期的功能而不管具体实现方式。JML把过程性的思考延迟到方法设计中,从而遵循了面向对象设计的一个原则即将过程性的思考尽可能地推迟。而且JML语言为了描述时清晰简洁,引入了大量描述行为的结构,比如模型域、量词、断言可视范围、预处理、后处理、条件继承、异常行为等规范。JML语言有很多优势:程序架构进行升级时降低引入BUG的概率;对每一部分可以进行单独检测;方便程序员之间的交流等等。因此JML语言的使用逐渐成为了当今的流行趋势。

 应用工具链

  无论是IDEA还是Eclipse,都提供了与JML语言相关的插件。

    OpenJML可以根据配置的solver文件检查JML描述语言的语法正确性、程序代码的实现是否满足JML语言所描述的设计的规格,并且可以提示方法中存在的可能影响程序运行的问题。

    Junit也是和JML相关的插件,JML负责对一个方法的功能进行描述,Junit则负责单独测试该方法的正确性。Junit可以帮助程序员对程序进行无死角的测试,大型工程中通过这种方法可以准确的定位出程序的BUG。测试时输入标准输入和对应的标准输出,当程序运行的结果和标准输出不同时Junit就会显示出不同的位置。JML Unit还可以根据JML语言自动生成测试数据,使用方便。

    Javadoc是提供编写java程序注释模板的一个插件,JML语言本身也是注释,所以可以通过javadoc先编写一个JML的大致注释模板,使用时直接调用该模板,在此模板上进行具体的实现,可以较好地保证JML语法的正确性。


前景

  由于openjml检测时不能出现exists和forall语法,官方提供接口中规格描述基本用到了上述两个语法,本人代码实现时容器没有完全按照规格描述设计,所以我选择验证自己写的方法,补充相应的可以检测的规格。

  Demo类类似于作业中的Path,有一个数组存所有节点值,方法包括获得数组长度,获得指定下标节点,判断数组有效性,获得数组中最大的节点,判断两个类是否相等(依据为类相同且最大的节点相同即可)

二.部署SMT Solver

前期代码如下,输入java -jar openjml-0.8.42-20190401/openjml.jar graph/Demo.java进行JML语法的检查
import java.util.ArrayList;

public class Demo {
    //@ public instance model non_null int[] modes;
    private /*@[email protected]*/ ArrayList<Integer> nodes;

    //@ ensures \result == nodes.size();
    public /*@[email protected]*/int size() {
        return nodes.size();
    }

    /*@ requires index >= 0 && index < size();
     @ assignable \nothing;
     @ ensures \result == nodes.get(i).intValue();
     @*/
    public /*@[email protected]*/ int getNode(int index) {
        return nodes.get(index);
    }

    //@ ensures \result == (nodes.size() >= 2);
    public /*@[email protected]*/ boolean isValid() {
        if (nodes.size() >= 2) {
            return true;
        } else {
            return false;
        }
    }

    //@ ensures \result == (max int i; 0 <= i && i < nodes.size(); nodes.get(i).intValue());
    public /*@[email protected]*/ int maxNode() {
        int max = nodes.get(0);
        for (int i = 0; i < nodes.size(); i++) {
            if (max < nodes.get(i)) {
                max = nodes.get(i);
            }
        }
        return max;
    }

    /*@ also
      @ public normal_behavior
      @ requires obj != null && obj instanceof Demo;
      @ assignable \nothing;
      @ ensures \result == (((Demo) obj).nodes.size() == nodes.size()) &&
      @                      ((Demo) obj).maxNode() == maxNode());
      @ also
      @ public normal_behavior
      @ requires obj == null || !(obj instanceof Demo);
      @ assignable \nothing;
      @ ensures \result == false;
      @*/
    public boolean equals(Object obj) {
        int flag = 0;
        if (obj != null && obj instanceof Demo) {
            Demo nobj = (Demo) obj;
            if (nobj.maxNode() == maxNode()) {
                flag = 1;
            }
        }
        if (flag == 1) {
            return true;
        } else {
            return false;
        }
    }
}
初次运行命令行检查规格正确性

报错检验后发现存在三个错误:1.29行的  //@ ensures \result == (max int i; 0 <= i && i < nodes.size(); nodes.get(i).intValue());  max前没有加‘\‘              2.45行的  @                 ((Demo) obj).maxNode() == maxNode());  (((Demo  少一个左括号,括号不匹配              3.14行的  @ ensures \result == nodes.get(i).intValue();   不应该用i而是index  get(index)更改后再次运行命令行不再报错接着输入命令  java -jar openjml-0.8.42-20190401/openjml.jar -rac graph/Demo.java 运行时检查根据警告删除第四行  //@ public instance model non_null int[] modes;再次运行时检查不再报错

三.JML Unit自动测试

  根据上述检测语法保证正确后,自动生成监测数据进行测试。由于JML不支持new Arraylist语法,用上述样例生测试测代码会造成nodes是一个空数组,里面没有元素,所以方法检测没有多大意义,下图是自动检测结果。

为了能够体现出该工具真正功能,我写了个简单的乘法样例。

四.架构设计

  本单元三次作业的架构设计除了要满足JML语言中各个函数描述的所有功能,还要考虑大量数据进行测试时程序的CPU运行时间,不能超过作业要求的最长时间。

  第九次作业为单元起始作业,功能较为简单,添加路径,删除路径,查找路径,比较路径,路径数量,路径中节点数量,计算总结点数量,路径是否包含特定节点。测试数据中有大量的数据,每条路径中有大量的节点,为了减少运行时间必然要选取合适的容器存储数据,我使用的是Hashmap,路径做键,对应id做值,用hashmap的原因是查找所需时间少,想通过hashcode判断,再通过equals函数,不需要直接对PathContainer进行遍历,对每个路径中所有节点一一比对,同时我在PathContainer中添加了一个path和int类型成员变量,当查到对应路径时,赋上查找结果,这样删除时不需要再次查找;最耗时的指令就是计算PathContainer中所有节点数量,我专门设置了一个叫total的hashmap,节点做键,出现次数做值,每次添加和删除路径时对total进行更新,查询总结点数量时直接输出total长度而不是遍历所有path计算,每个path中也有一个hashmap存path里面的所有节点以及出现次数,提前算好结果需要时直接取而不是需要时再计算,这种思想在后两次作业中也得到了大量运用,这样的做法需要所有存数据的容器在add或者remove路径时均需要更新。

  第十次作业增加了四个指令,容器中是否存在一个节点,是否存在一条边,两个节点是否连通,两个节点最小距离。由于已经有total存容器中节点和出现次数,对total用contains方法可以直接判断是否存在一个节点。对于边的出现我新建了一个Edge类,存着一条边两端的两个节点,类似于节点的处理,在Path类和Graph类里各增加一个hashmap,以边做键,边出现的次数做值,对tedge用contains方法可以直接判断边是否存在;为了节省判断两个节点是否连通的时间,新建一个叫graph的arraylist,里面每一个元素是一个hashset,存着一个连通块中所有节点,每次遍历graph,只要在其中一个hashset中同时出现两个节点,则节点相连;算最小距离,权重均相同默认为1,所以我采用BFS算法,为了不出现静态数组,新建一个叫idreach的hashmap当作邻接数组使用,节点做键,和该节点邻接的所有节点构成的hashset做值,idreach容器存放数据可以满足BFS的需要。

  第十一次作业增加四个指令,连通块数量,最小换乘,最小票价,最低不满意度。第十次的graph的size为连通块数量;最小换乘,新建一个叫station的hashmap,节点做键,该节点所在的所有path的id构成的hashset做值,换乘次数首先置0,先遍历一个节点中的所在的所有path,如果有另一个节点直接返回换乘次数,没有则换乘次数++,再次遍历同path中所有的节点所处的所有path,往复直至一个path中有另一个节点;最小票价和最低满意度都涉及到换乘去计算权重,而且可以同一个path内部换乘,这种情况还不算换乘,最后我采取讨论区里不拆点做法,先对每一个path内部用Floyd算法算出path内部最小票价和不满意度,path内部还用一个hashmap存真实节点和数组下标的映射关系,在RailwaySystem内部新增两个静态数组分别管理票价和不满意度,也新增一个叫mapping1的hashmap存映射关系,计算时对两个二维数组用迪杰斯特拉算法,最后分别减2和32即可。

  每次作业的重构最主要的就是为新方法添加新容器,并且对add path和remove path方法进行更改从而能够对新容器进行更新(更新顺序也可能需要更改)。

五.代码Bug

  三次强测最后都没有出现问题,得益于舍友写的硬核评测机,但是自己课下也遇见了bug。

  1.对于二维数组初始无穷大值一开始赋为INT表示最大范围,发现计算结果与预期不符,因为对0x7fffffff进行加时会立马变成负数,此时比较无穷大就变成一个小于0的数,后来将初值变为10000000,因为这个常数也比正常结果大得多。

  2.add和remove路径时更新各个容器的顺序不当也会导致bug的出现,为了减少容器更新时的复杂度,部分容器更新时并没有对所有path遍历,但是相应的对正确性要求就更高。

  3.对于hashset,hashmap的clone方法使用。如果需要取出一个hashmap,运算时对其进行更改从而出现结果,又不能影响原有hashmap中的内容,此时应该使用clone方法clone一个新容器保证内容完全复制,如果只是用一个hashmap指向要更改的hashmap,运算更改内容的同时原有的容器内容也会被更改,后期再用这个容器时里面的内容就和预期出现不符造成结果错误。

六.心得体会

 规格撰写

  JML语言在我看来很简单,内容并不多,一共只有JML表达式,方法规格,类型规格这三大主项,每一个中又有几个小的知识点,最常用的是JML表达式中的内容,它就相当于java语言中出现的基本参数类型和语法。对于大部分同学而言,给出JML语言可以很好地理解函数的规格和具体的作用,但是如果给一个函数去写对应的JML语言,还是一个难题,尤其是当这个函数十分复杂的时候,当然这一单元的三次作业不需要我们撰写JML语言,但为了以后程序员之间代码的互写,这一技能还是很有必要去练习的。对于特别复杂的函数撰写规格,老师们用第十一次作业告诉我们,可以对复杂的函数进行拆分成几小块,单独进行填写,复杂函数JML语言直接调用拆分部分即可。

 个人理解

  JML语言可以很好的用来描述一个函数的功能,不同程序员之间不需要完全理解程序设计架构,只需要根据JML所规定的语法进行函数的编写,只要满足JML语言就可以确保程序的正确性,是一种十分方便的语法。助教在群中说过函数具体的实现方式是任意的,并不需要完全按照规格描述执行,所以程序员有着极大的可操作性,所以JML重要性不言而喻,值得拿出一个单元专门训练。

原文地址:https://www.cnblogs.com/17373395c/p/10897869.html

时间: 2024-07-30 12:14:35

第三单元JML规格总结的相关文章

2019年北航OO第三单元(JML规格任务)总结

一.JML简介 1.1 JML与契约式设计 说起JML,就不得不提到契约式设计(Design by Contract).这种设计模式的始祖是1986年的Eiffel语言.它是一种限定了软件中每个元素所必需的责任与义务的开发模式,程序设计中的每个元素都需要用规范的语言精准地限定其前置条件(Preconditions).后置条件(Postconditions)和不变式(Invariants).通过这三项限定,我们可以清晰地获得对一个函数功能的刻画,从而达成设计与实现的分离,便于优化.测试和生成文档.

面向对象第三单元(JML)总结体会

一.JML语言 定义 Java建模语言(JML)是一种行为接口规范语言,可用于指定Java模块的行为 .它结合了Eiffel的契约方法设计 和Larch 系列接口规范语言的基于模型的规范方法 . 理论基础 JML是契约式语言的一种具体表现形式. 契约(Contact):声明一个函数/方法的时候,对函数的输入和输出所具备的性质是有所期望和规定的.有时候这种性质会被我们明确的写出来,有时候会被我们忽略掉.这些期望和规定就是Contract. 而契约设计的核心便是断言(assertion) :永远为真

OO第三单元总结 JML

OO第三单元总结 JML JML语言的理论基础.应用工具链情况 JML是一种形式化的,面向JAVA的行为接口规格语言,它结合了Eiffel的契约方法和Larch方法,以及细化演算的一些元素,有着坚实的理论基础. JML最主要的语法有前置条件,后置条件,不变式,通过这些语法对输入和输出进行约束,也就是达成了一种契约.当模块实现后,只要输入输出满足这些约束表达式就满足了规格的要求.JML主要使用java的语法,除此之外还有自己的一些语法,比如/forall,/exist等等,来实现对输入输出的约束.

OO第三单元总结(规格设计)

OO第三单元总结 一.关于JML Java Modeling Language,即JML是一种规格化表示语言,主要用于对Java程序的各种方法功能的规范描述.这样做既可以给程序设计人员明确清晰的功能要求,又可以充分全面地验证已有的代码实现保证其满足规格描述的要求. 1.语法梳理 JML的语法清晰直观地描述了一个Java的各种特征.它的语法主要由以下三个部分组成. (1)表达式: 诸如 \result \old等有具体确定意义的固定关键词称为表达式.通过不同的搭配组合可以表示不同的含义,比如(\f

OO第三单元总结--根据JML写代码

一. JML语言 1. 理论基础 首先,JML不是JAVA的一部分,它是一群研究者为JAVA设计的扩展部分,但还没有得到官方的支持.因此,JAVA编译器并不支持JML,所以要想JML起作用,只能采用类似openJML这样的第三方来编译,将JML 规格编译为运行时检查的语句,即RAC code(runtime assertion checking).如果代码实现与其JML规格不一致,将引发运行时JML exception. JML遵从契约式设计范式(DBC),Design by contract是

OO第三单元总结

JML语言理论基础 Java建模语言(Java Modeling Language,JML)是一种进行详细设计的符号语言,他鼓励你用一种全新的方式来看待Java的类和方法.JML是一种行为接口规格语言 (Behavior Interface Speci?cation Language,BISL),基于Larch方法构建.BISL提供了对方法和类型的规格定义手段.所谓接口即一个方法或类型外部可见的内容.通过在Java代码中增加了一些符号,这些符号用来标识一个方法是干什么的,却并不关心它的实现.使用

hOmewOrk 第三单元 总结

hOmewOrk 第三单元 总结 JML理论基础梳理 JML是用于对Java程序进行规格化设计的一种表示语言. 1. 注释结构 JML表示规格的内容包含在注释之中.可以使用行注释和块注释.行注释的表示方式为 //@annotation ,块注释的方式为 /* @ annotation @*/ . 2. JML表达式 JML表达式是在基于JAVA语法基础上,新增了一些操作符和和原子表达式组成的. 2.1 原子表达式 \result表达式:表示方法执行后的返回值. \old( expr )表达式:用

第三单元总结

第三单元总结 JML相关 一 梳理JML语言的理论基础.应用工具链情况 JML是一种形式化的, 面向JAVA的行为接口规格语言( behavioral interface specification language) JML允许在规格中混合使用Java语法成分和JML引入的语法成分. JML主要是实现了设计与实现相分离, 使得设计时不会陷入实现的困难中去. 实现时, 由于JML实现已经设计完整, 也不必担忧设计上的缺陷. JML相关的工具主要有OpenJML和JMLUnitNG, 前者类似于一

规格化设计——OO第三单元总结

规格化设计--OO第三单元总结 一.JML语言理论基础.应用工具链 1.1 JML语言 ? JML(java modeling language)是一种描述代码行为的语言,包括前置条件.副作用等等.JML是一种行为接口规格语言 (Behavior Interface Speci?cation Language,BISL),基于Larch方法构建. ? 通过使用JML,我们可以忽略一个类.一个方法内部的具体实现,专注于描述方法的预期功能,从而把过程性的思考延迟到方法设计中,扩展了面向对象设计的原则