OO第三单元总结

Posted 2021-12-02 nebulau

JML语言理论基础

Java建模语言（Java Modeling Language，JML）是一种进行详细设计的符号语言，他鼓励你用一种全新的方式来看待Java的类和方法。JML是一种行为接口规格语言 （Behavior Interface Speci?cation Language，BISL），基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。通过在Java代码中增加了一些符号，这些符号用来标识一个方法是干什么的，却并不关心它的实现。使用JML，我们就能够描述一个方法的预期的功能而不管他如何实现。通过这种方式，JML把过程性的思考延迟到方法设计中，从而扩展了面向对象设计的这个原则。

JML以javadoc注释的方式来表示规格，每行都以@起头。有两种注释方式，行注释和块注释。JML引入了大量用于描述行为的结构，比如有模型域、量词、断言可视范围、预处理、后处理、条件继承以及正常行为（与异常行为相对）规范等等。对代码进行抽象：

方法规格抽象  

• 执行前对输入的要求----前置条件(requires) 
• 执行后返回结果应该满足的约束----后置条件(ensures) 
• 副作用范围限定，assignable列出这个方法能够修改的类成员属性
• 规格中专门说明exceptional_behavior 

数据(类型)规格抽象

• 数据状态应该满足的要求----不变式(invariant) 
• 数据状态变化应该满足的要求----约束(constraint) 

通过一系列的JML表达式实现描述：

原子表达式

• \result表达式：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。
• \old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值。
• \not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。
• \not_modi?ed(x,y,...)表达式：与上面的\not_assigned表达式类似，该表达式限制括号中的变量在方法执行期间的取 值未发生变化。
• \nonnullelements( container )表达式：表示 container 对象中存储的对象不会有 null 。
• \type(type)表达式：返回类型type对应的类型(Class)。
• \typeof(expr)表达式：该表达式返回expr对应的准确类型。

量化表达式

• \forall表达式：全称量词修饰的表达式。
• \exists表达式：存在量词修饰的表达式。
• \sum表达式：返回给定范围内的表达式的和。 
• \product表达式：返回给定范围内的表达式的连乘结果。
• \max表达式：返回给定范围内的表达式的最大值。 
• \min表达式：返回给定范围内的表达式的最小值。 
• \num_of表达式：返回指定变量中满足相应条件的取值个数。

JML应用工具链

JML相应的工具链，可以自动识别和分析处理JML 规格。常用的有openjml，其使用SMT Solver来对检查程序实现是否满足所设计的规格(specification)。目前openjml封装了四个主流的solver：z3, cvc4, simplify, yices2。z3由Microsoft开发的，并已在github上开源：https://github.com/Z3Prover/z3 其正式发布版可通过https://www.microsoft.com/en-us/download/details.aspx?id=52270获得。cvc4由Standford开发，可以通过http://cvc4.cs.stanford.edu/downloads/下载。 

SMT Solver的部署

下载openjml在IDEA中配置外部工具链进行静态验证。

部署JMLUnitNG/JMLUnit

JUnit是一个强大的单元测试工具。配置过程如下：

1、下载JUnit4.13的jar包

2、把这两个jar包加入环境变量的classpath中

3、安装IDEA的Junit generator V2.0插件

4、设置项目jar包依赖

5、生成一个Test类模板

6、运行测试

部分测试如下：

import com.oocourse.specs2.models.Path;
import org.junit.After;
import org.junit.Assert;
import org.junit.Before;
import org.junit.Test;

/**
 * MyGraph Tester.
 *
 * @author <Authors name>
 * @version 1.0
 * @since <pre>五月 20, 2019</pre>
 */
public class MyGraphTest {
    private MyGraph myGraph = new MyGraph();
    private Path path1, path2, path3, path4;

    @Before
    public void before() throws Exception {
        path1 = new MyPath(1, 2, 3, 4);
        path2 = new MyPath(1, 2, 3, 4);
        path3 = new MyPath(1, 2, 3, 4, 5);
        path4 = new MyPath(2, 5, 6, 8, 9);
        myGraph.addPath(path1);
        myGraph.addPath(path2);
        myGraph.addPath(path3);
    }

    @After
    public void after() throws Exception {
    }

    /**
     * Method: size()
     */
    @Test
    public void testSize() throws Exception {
//TODO: Test goes here...
        Assert.assertEquals(myGraph.size(), 2);
    }

    /**
     * Method: containsPath(Path path)
     */
    @Test
    public void testContainsPath() throws Exception {
//TODO: Test goes here...
        Assert.assertTrue(myGraph.containsPath(path2));
    }

    /**
     * Method: containsPathId(int pathId)
     */
    @Test
    public void testContainsPathId() throws Exception {
//TODO: Test goes here...
        Assert.assertTrue(myGraph.containsPathId(2));
    }

    /**
     * Method: getPathById(int pathId)
     */
    @Test
    public void testGetPathById() throws Exception {
//TODO: Test goes here...
        Assert.assertEquals(myGraph.getPathById(2), path3);
    }

    /**
     * Method: getPathId(Path path)
     */
    @Test
    public void testGetPathId() throws Exception {
//TODO: Test goes here...
        Assert.assertEquals(myGraph.getPathId(path2), 1);
    }

    /**
     * Method: addPath(Path path)
     */
    @Test
    public void testAddPath() throws Exception {
//TODO: Test goes here...
        Assert.assertEquals(myGraph.addPath(path3), 2);
    }

    /**
     * Method: removePath(Path path)
     */
    @Test
    public void testRemovePath() throws Exception {
//TODO: Test goes here...
        Assert.assertEquals(myGraph.removePath(path2), 1);
    }

    /**
     * Method: removePathById(int pathId)
     */
    @Test
    public void testRemovePathById() throws Exception {
//TODO: Test goes here...
        myGraph.removePathById(1);
        Assert.assertTrue(!myGraph.containsPath(path2));
    }

    /**
     * Method: getDistinctNodeCount()
     */
    @Test
    public void testGetDistinctNodeCount() throws Exception {
//TODO: Test goes here... 
    }

} 

经验证，功能得到实现且未发现错误。

架构设计的思考

第二次Graph继承第一次PathContainer实现。采用数据结构如下：

/*
    node counter;
    pid -- path Map;
    distinctNodesSet;
    graph邻接表;
     */
    private int cnt = 1;//路径id计数器
    private Map<Integer, Path> pathMap;//路径id-路径对应表
    private Set<Integer> nodeSet;//不重复的节点集合
    private Map<Integer, HashSet<Integer>> adj;//图的邻接表
    /*
    used for graph calculate
     */
    private Map<Integer, Integer> marked;//bfs记录访问状态
    private Map<Integer, Integer> distTo;//bfs记录距离

无权无向图，简单bfs即可寻找最短路径。第三次规格作业尝试采用Floyd寻找几种自定义最短路。

bug分析

第一次规格作业，偏序比较接口未考虑int溢出，没有直接使用Integer.compareTo，加上TLE共计8处bug，第二次作业1次TLE的bug。

心得体会

此单元主要学习规格的理解和使用，初步了解需求分析到代码的中间过程---即规格的标准和工具，逐渐理解JML等规格语言对于代码交接、维护的重要意义。JML像是一种契约，在你完成你的工作后来调用我，我就保证返回给你正确的结果，这种契约保证了软件、工程开发的各司其职、高效执行。