zoukankan      html  css  js  c++  java
  • BUAA-OO-JML

    BUAA-OO-JML

    JML 概念与 toolchain

    JML 是一种为 Java 程序设计的、遵循 design by contract 范式的、基于 Hoare Logic 构建的 behaviour interface specification language。它通过使用 Hoare style precondition、postcondition and invariants 为程序员提供了一套规范而清晰地描述 Java 模块的方法,并提供了可形式化验证的可能。

    与 JML 相配套的,是各种的 verification tools 和单元测试生成工具,包括但不限于:OpenJML,Krakatoa,ESC,KeY,JMLUnit(停止维护,支持至JAVA1.4),JMLUnitNG。

    作业架构设计分析

    第一次作业

    类图如下:

    其中 Utils 类是提供各种常用静态方法的类,譬如 getKeyByValue ,getEntryByValue 等方法。下同。

    可以看出来,基本和课程组提供的接口是一致的,没有做扩展。

    第二次作业

    类图如下:

    可以看出来,基本和课程组提供的接口是一致的,没有做扩展。

    第三次作业

    类图如下:

    为了支持新需求,加入了 DijkstraSovler 类和 Tuple 类,前者用于统一最短路求解框架,后者为前者求解提供中间辅助。

    但是,比较好的架构应是增加一个 Node 类,用以记录某个 Node 的 ID 和所属 PathID,在 Dijkstra 算法执行中,这两者都是关键且是一起出现的要素。

    心得体会

    关于 JML 的撰写,由于是基于 Hoare Logic,可以分为以下三部分来进行考虑:

    • precondition: 函数进入前需要满足的条件。
    • postcondition: 函数退出后需要满足的条件。
    • assertion: 函数途中需要满足的条件。

    对于一份普通的 Java 代码,automatic verification tools 是无法通过简单地分析其 flow 来获知里面各个 components 的功能以及之间的关系。为了能够使得测试自动化、全面化、逻辑化,引入 JML 来描述 components 的功能是有必要的。

  • 相关阅读:
    ZOJ 1403 解密
    HDU 1021 斐波那契
    Wannafly挑战赛26题解
    NOI2019省选模拟赛 第三场
    NOI2019省选模拟赛 第五场
    洛谷P5280 [ZJOI2019]线段树(线段树)
    NOI2019省选模拟赛 第六场
    Wannafly挑战赛29题解
    李超线段树学习笔记
    洛谷P4069 [SDOI2016]游戏(李超线段树)
  • 原文地址:https://www.cnblogs.com/btapple/p/10902665.html
Copyright © 2011-2022 走看看