OO第三单元总结

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像是一种契约，在你完成你的工作后来调用我，我就保证返回给你正确的结果，这种契约保证了软件、工程开发的各司其职、高效执行。

原文地址：https://www.cnblogs.com/nebulau/p/10896248.html

时间： 2024-10-04 04:45:59

OO第三单元总结的相关文章

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

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

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第三单元总结-规格化设计

OO规格化编程体验小结 1. JML语言的理论基础.应用工具链情况 JML 理论基础: JML建立契约式编程的基础上,是一种实现契约式编程的规格化语言.顾名思义,契约式编程,是供求双方建立在一定的契约上进行软件的开发和应用.类似于在共同完成这一个工程的时候我们对于每个方法都以一个供求双方都统一并且详细知晓的合同,在这个合同上,供应方要不多不少完成合同上的所有要求,需求方的可提出的需求范围只限于合同上的明确条文.这样同时明确了双方的权利和义务.而产生契约式编程的背景是很多工程的开发过程权责混乱,导

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

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

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知识梳理 部署JMLUnitNG/JMLUnit 按照作业梳理自己的架构设计,并特别分析迭代中对架构的重构 按照作业分析代码实现的bug和修复情况 阐述对规格撰写和理解上的心得体会 JML知识梳理 JML理论基础 关于JML的相关介绍其实课程给出的指导书就已经足够使用了,由于指导书上都有相关知识的梳理,所以这里不花费大量篇幅去书写这部分内容,只是简单提及一些东西.首先是什么是JML,课程进行,其实阅读简单的JML已经没有多大障碍了,但是对于JML的定义这种概念已经忘记的差不多了.JM

OO第三单元总结——java建模语言

一.JML语言的理论基础 面向对象分析和设计的原则之一就是应当尽可能地把过程设想往后推.我们大多数人只在实现方法之前遵守这一规则.一旦确定了类及其接口并该开始实现方法时,我们就转向了过程设想. Java 建模语言(JML)将注释添加到 Java 代码中,这样我们就可以确定方法所执行的内容,而不必说明它们如何做到这一点.有了 JML,我们就可以描述方法预期的功能,无需考虑实现.通过这种方法,JML 将延迟过程设想的面向对象原则扩展到了方法设计阶段. 二.JML应用工具链 openJML可以检查规格

OO第三单元博客总结

原文地址:https://www.cnblogs.com/xiongmaoage/p/10903350.html