目录

  • OO第三单元总结

    • 1. JML语言理论基础以及应用工具链情况梳理
    • 2. OpenJML的简单使用:部署、验证及结果分析
    • 3. JMLUnit的使用:部署、验证及结果分析
    • 4. 作业架构设计梳理
    • 5. bug分析及修复情况
    • 6. 心得体会

OO第三单元总结

1. JML语言理论基础以及应用工具链情况梳理

1.1 JML语言理论基础

​ JML(Java Modeling Language)是一种用于规范Java程序行为的行为接口规范语言。JML为方法和类型的规格进行定义,为程序的形式化验证提供了基础,通过工具链可以实现静态检查和自动测试数据生成。

注释结构

  • 行注释: // @ annotation
  • 块注释:/* @ annotation @*/

JML表达式

  • 原子表达式

    • \result,\old( expr )
  • 量化表达式
    • \forall表达式:全称量词修饰的表达式
    • \exists表达式:存在量词修饰的表达式
    • \sum表达式:返回给定范围内的表达式的和
    • \max表达式:返回给定范围内的表达式的最大值
    • \min表达式:返回给定范围内的表达式的最小值
  • 集合表达式
    • 可以在JML规格中构造一个局部的集合(容器),明确集合中可以包含的元素。
  • 操作符
    • 子类型关系操作符: E1<:E2 ,
    • 等价关系操作符: b_expr1<==>b_expr2 或者 b_expr1<=!=>b_expr2
    • 推理操作符: b_expr1== >b_expr2 或者 b_expr2< ==b_expr1
    • 变量引用操作符:\nothing指示一个空集;\everything指示一个全集

方法规格

  • 前置条件(pre-condition)

    • 通过requires子句来表示: requires P;
  • 后置条件(post-condition)
    • 通过ensures子句来表示: ensures P;
  • 副作用范围限定(side-effects)
    • 使用关键词 assignable 或者 modifiable

类型规格

  • 不变式invariant
  • 状态变化约束constraint

1.2 工具链简介

与规格化设计相关的工具主要有:OpenJML, JMLUnit, TestNG等等。

  • OpenJML

对Java 编译器将带有 JML 规范注释的 Java 程序编译成 Java 字节码。 编译的字节码包括检查的运行时断言检查指令。

  • JMLUnit与TestNG

JMLUnit 与 TestNG主要是基于JML规格生成样例并自动化进行单元测试

2. OpenJML的简单使用:部署、验证及结果分析

参考伦佬的贴子。

2.1 JML规格语法check

源码
public class Demo {/*@@ public normal_behaviour@ requires lhs<0 &&*/public static int compare(int lhs, int rhs) {return lhs - rhs;}public static void main(String[] args) {compare(114514, 1919810);}
}
结果分析
$ ./openjml -check Demo.java
Demo.java:5: 错误: The type or expression near here is invalid (or not implemented): ( token <JMLEND> in JmlParser.term3())*/^
1 个错误

检测出JML表达式无效。

2.2 基于OpenJML的静态bug检测

源码
public class Demo {/*@@ public normal_behaviour@ requires lhs > rhs;@ ensures \result > 0;@ also@ requires lhs < rhs;@ ensures \result < 0;@ also@ requires lhs == rhs;@ ensures \result == 0;@*/public static int compare(int lhs, int rhs) {return lhs - rhs;}public static void main(String[] args) {compare(114514, 1919810);}
}
结果分析
$ ./openjml -check Demo.java
$ ./openjml -esc Demo.java
Demo.java:14: warning: The prover cannot establish an assertion (ArithmeticOperationRange) in method compare:  underflow in int differencereturn lhs - rhs;^
demo/Demo.java:14: warning: The prover cannot establish an assertion (ArithmeticOperationRange) in method compare:  overflow in int differencereturn lhs - rhs;^
2 warnings

检测结果显示JML表达式合法,但存在减法溢出的漏洞。

2.3 运行时检查

源码
public class Demo {/*@@ public normal_behaviour@ requires lhs > rhs;@ ensures \result > 0;@ also@ requires lhs < rhs;@ ensures \result < 0;@ also@ requires lhs == rhs;@ ensures \result == 0;@*/public static int compare(int lhs, int rhs) {return lhs - rhs;}public static void main(String[] args) {compare(2147483647, -2147483647);}
}
结果分析
94831@LAPTOP-35U6BFJF MINGW64 /d/MyCollege/CourseCenter/Semester4/CC/OO/JML/testOpenJml
$ ./openjml -rac Demo.java94831@LAPTOP-35U6BFJF MINGW64 /d/MyCollege/CourseCenter/Semester4/CC/OO/JML/testOpenJml
$ java -Djava.ext.dirs=lib Demo
Demo.java:14: 警告: JML result of numeric operation is out of range of the target typereturn lhs - rhs;^
Demo.java:13: 警告: JML postcondition is falsepublic static int compare(int lhs, int rhs) {^
Demo.java:5: 警告: Associated declaration: Demo.java:13: 注:@ ensures \result > 0;^

openjml 的使用和 javac 大致相同,先编译后运行即可。结果显示出现了减法溢出的情况。

3. JMLUnit的使用:部署、验证及结果分析

参考伦佬的贴子——第二篇。

以下是针对MyPath中的部分方法进行测试

3.1 生成测试文件

3.2 编译

编译部分共分为两步:

  • 用 javac 编译 JMLUnitNG 的生成文件
  • 用 jmlc 编译自己的文件,生成带有运行时检查的 class 文件
94831@LAPTOP-35U6BFJF MINGW64 /d/MyCollege/CourseCenter/Semester4/CC/OO/JML/testOpenJml
$ javac -cp jmlunitng.jar src/*.java94831@LAPTOP-35U6BFJF MINGW64 /d/MyCollege/CourseCenter/Semester4/CC/OO/JML/testOpenJml
$ ./openjml -rac src/MyPath.java

3.3 测试及结果分析

94831@LAPTOP-35U6BFJF MINGW64 /d/MyCollege/CourseCenter/Semester4/CC/OO/JML/testOpenJml/src
$ java -Djava.ext.dirs=../lib MyPath_JML_Test
[TestNG] Running:Command line suitePassed: racEnabled()
Failed: constructor MyPath(null)
Skipped: <<null>>.containsNode(-2147483648)
Skipped: <<null>>.containsNode(0)
Skipped: <<null>>.containsNode(2147483647)
Skipped: <<null>>.getDistinctNodeCount()
Skipped: <<null>>.getNode(-2147483648)
Skipped: <<null>>.getNode(0)
Skipped: <<null>>.getNode(2147483647)
Skipped: <<null>>.isValid()
Skipped: <<null>>.size()===============================================
Command line suite
Total tests run: 11, Failures: 1, Skips: 9
===============================================

​ 由结果可知,MyPath的构造未通过测试,经查,发现,当传进来的nodeList为空时,在 nodeList.length 时可能会发生访问空指针的错误。

    public MyPath(int... nodeList) {for (int i = 0; i < nodeList.length; i++) {myNodes[i] = nodeList[i];}}

4. 作业架构设计梳理

4.1 第一次作业

分析

第一次作业较为简单,利用好HashMap实现 O(1) 的查询即可。

类图如下:

  • MyPath

    • 使用 ArrayList<Integer> nodes 结构保存节点序列
    • 使用 HashMap<Integer, Integer> nodesMap 来保存结点及结点在path中的出现次数,以便由 nodesMap.size() 直接 getDistinctNodeCount()
  • MyPathContainer
    • 使用 HashMap<Integer, MyPath> id2PathHashMap<MyPath, Integer> path2Id 两个HashMap来实现 PathPathId 的双向映射,从而快速索引。

4.2 第二次作业

分析
  • 第二次作业在 PathContainer 的基础上新增了 Graph 接口,MyPathContainer无需重构,直接继承即可。
  • 需要注意的是由于增删指令不超过80条,查询指令将接近7000条,而评测又严格限制CPU时间,因此最短路的计算就需要一定的策略了。考虑到查询指令数,如果采用Floyd每次都把所有结点的最短路算出来,将会产生大量的性能浪费,同时由于其O(n^3)的复杂度,因而弃用。
  • 考虑到第二次作业为无边无权图,本人采用 BFS + Lazy Search 算法。即类似缓存机制,将答案存储在“TLB”中,每次进行增删操作时由于图结构改变,需要清空TLB。每次查询先查TLB,若命中,直接返回;若MISS,就BFS一下同时更新TLB。

类图如下:

  • Edge

    • 抽象出来的无向边,存储两个结点以及边权(本次作业恒为1)
    • 重写equals及hashcode方法
  • MyGraph
    • 使用 HashMap<Integer, Integer> nodeMapHashMap<Edge, Integer> edgeMap 来存储结点和边及其度数
    • HashMap<Edge, Integer> weightHashMap<Edge, Integer> shortestDist 分别存储权重即相应的最短路

4.3 第三次作业

​ 本次作业难度有了较大的提升,且由于当周冯如杯答辩等原因导致时间紧迫,加上周一晚上盲从讨论区大佬的观点。在没有完全参悟拆点法的情况下,临时更换策略极限重构,结果在建图时遇到了很大的困难,最后因为时间关系草草完成了图的构建,由于结构混乱,且复杂度较高,导致强测大半CTLE。真应了助教那句:

“重构一时爽,一次重构火葬场”

​ 由于没有将图结构的存储与答案的存储分离开,导致二者的耦合度较高,维护成本非常大;
因而在认真研究了标程的架构设计后,重构了图的存储逻辑,借鉴了标程的工厂模式,如下。

分析
  • 本次作业采用了 拆点 + Dijkstra + Lazy Search,大体思路同上次作业,拆点遵从zyy大佬的2+x模式,具体见这里。
  • 难点之一在于四个最短问题的求解,而它们的主要区别在于邻接边与换乘边的权值不同,设邻接边权为x,换乘边权为y,则有:
    • 最短路径:x = 1, y = 0 // 实际上,最短路径的求解我仍然放在了 MyGraph 中
    • 最少换乘:x = 0, y = 1
    • 最低票价:x = 1, y = 2
    • 最小不满意度:x = MAX( F(fromNode), F(toNode) ), y = 32;
  • 难点之二则在于图的存储,本人采用了嵌套HashMap以邻接表的形式来存储。设计模式上,重构版采用了工厂模式,将三种最短问题抽象为同一种产品,不同的仅仅是 stepWeightswitchWeight,同时由于最少不满意度的邻接边权非固定值,需要单独对其进行拓展,处理 stepWeight 的求解。这里仅仅需要继承 RailwayGraphFactory即可,这样在 MyRailwaySystem 中只需要维护好这三个产品即可。
  • 跨越上面两座大山后,问题基本就已经解决了,唯一仍需注意的是Dijkstra的写法,本人原始写法在更新dist[]时是无脑遍历所有结点,而拆点法会导致节点数最大会达到4000+,因而时间巨慢。实际上,每次遍历只需要遍历离源点st最近结点vertex的可达集即可大大降低时间复杂度。
类图如下:

  • RailwayGraphFactory
    public static final int INFINITY = 0x3fffffff;private final int stepWeight;   // 邻接边权private final int switchWeight; // 换乘边权// <stNode, edNode> -> edgeWeightprivate HashMap<Node, HashMap<Node, Integer>> adjList = new HashMap<>();// <fromNode, toNode> -> shortest distanceprivate HashMap<Node, HashMap<Node, Integer>> ansMap = new HashMap<>();
  • MyRailwaySystem
/*   Abstract Graph  */
// <NodeId, stNode>     : pathId = 0
private HashMap<Integer, Node> stMap = new HashMap<>(); // 抽象起点
// <NodeId, edNode>     : pathId = -1
private HashMap<Integer, Node> edMap = new HashMap<>(); // 抽象终点/*   weight matrix  */
private RailwayGraphFactory transferMatrix;     // 最少换乘
private RailwayGraphFactory priceMatrix;        // 最低票价
private UnpleasantGraphFactory unpleasantMatrix;// 最小不满意度

5. bug分析及修复情况

  • 第一次作业中的compareTo出现了减法溢出错误。原因是采用了一种比较“取巧”的做法 return a-b;,由于第一次作业比较掉以轻心,没有进行有效的测试,导致强测WA了快一半点。修复时只需改用 if-else即可。
  • 第二次作业在强测与互测中均未被发现bug。
  • 第三次作业即在3.3陈述的CTLE错误,莫得办法,只能重构(捂脸),但在重构的过程中也确实有所收获。

6. 心得体会

​ 三周的JML之旅已然结束,这期间当然又踩了很多坑,也吃了不少经验教训。

​ 首先,给我留下印象最深刻的还是那句话,“重构一时爽,但也可能一次重构火葬场”。不过虽然如此,在重构的过程中也有了很多新的感悟与体会,一个优美的架构好处不仅仅在于其可扩展性,由于模块与模块之间耦合度低,逻辑重合度低,其bug调试及定位难度也大幅降低,同时也能更好的借助JUnit进行覆盖性测试。

​ 下面再来谈一谈对JML规格撰写的体会。

​ 通过查阅JML手册以及参考已有规格,为一个方法写一份简单的规格描述难度并不大,在几次上机中也并没有太大的问题,而想要针对某个特定项目写一份完整、严谨的规格却是十分困难的。但 JML 的好处在于,测试人员能够从设计层面直接判断方法的正确性,而不用花费大量时间阅读代码。同时由于其语法的严谨性、规范性,给开发人员也带来极大地便利,不需要再去啃模棱两可的指导书中的需求,专注于代码的编写,正如指导书所言,”只要你确保满足了JML的需求,那么你的程序一定是正确的“

​ 此外,通过对 JML 规格的阅读与撰写,我对每个方法的 Pre-Condition, Post-Condition, Side-Effect 有了更加深刻的理解,这是一个方法,或是一段程序正确性的根本保证,能更好地帮助我们判断一个架构设计的正确性与合理性。

​ 最后再谈一谈Openjml。本单元一开始对基于JML规格的形式化验证与自动化测试是充满期待的,但不得不说,JML的工具链使用体验极差,对语法的要求过于苛刻,导致写一份能够完美通过编译的JML规格的难度要远远大于完成程序本身,似乎有些本末倒置?但 JML 教给我们规格设计的思想以及这种规范编程的思维方式,对我们的程序员进化之路是大有裨益的。

​ 国际惯例,祝OO课程越来越好!

转载于:https://www.cnblogs.com/puzzledAtticus/p/10908088.html

OO之旅——JML篇相关推荐

  1. React Native填坑之旅--动画篇

    React Native填坑之旅--Button篇 React Native填坑之旅--动画 React Native填坑之旅--HTTP请求篇 动画是提高用户体验不可缺少的一个元素.恰如其分的动画可 ...

  2. 第一学期ACM之旅总结篇

    是我大一第一学期ACM之旅总结篇鸭,纪念逝去的青春: 自加入ACM集训队以来已有三个月之久,虽然一开始什么都不懂,但对ACM充满期待与向往.入队以后,通过和队员们一起学习以及各个学长的指导下,我慢慢地 ...

  3. Linux之旅----硬件篇

    linux之旅----硬件篇(DIY) 记得第一次接触电脑应该是小学三年级,那时候的它对我来说只是一个游戏机的概念:极品飞车.红色警戒.CS.热血传奇.......陪我度过了小学懵懂的时光:泡泡堂.梦 ...

  4. CTF之旅WEB篇(3)--ezunser PHP反序列化

    一.审题 对方朝你扔过来一串代码(当然这次又是蹭的题只说过程和思路): <?php highlight_file(__FILE__); class A{public $name;public $ ...

  5. ABAP项目砖家之旅-基础篇

    ABAP项目砖家之旅-基础篇 前言 一.ABAP简介 二.ABAP开发工具 1.SAPgui 2.eclipse和HANA studio 三.相关搬砖经验 1.必须还是熟悉语法 2.复制粘贴写注释 3 ...

  6. ESP8266开发之旅 网络篇⑭ web配网

    文章目录 1. 前言 2. Web配网(AP配网) 2.1 自定义AP配网 2.2 WiFiManager 3. 总结 授人以鱼不如授人以渔,目的不是为了教会你具体项目开发,而是学会学习的能力.希望大 ...

  7. [OO] Unit3 Summary JML系列

    文章目录 [OO] Unit3 Summary JML系列 JML理论基础 优点 语法基础 常用表达式 方法规格 类型规格 JML工具链 测试工具使用报告 SMT Solver EvoSuite JM ...

  8. ESP8266开发之旅 应用篇⑭ 局域网应用 ——炫酷RGB彩灯(WebSocket实现)

    文章目录 1.前言 2.技术原理 3.ESP8266 源码 4. APP 授人以鱼不如授人以渔,目的不是为了教会你具体项目开发,而是学会学习的能力.希望大家分享给你周边需要的朋友或者同学,说不定大神成 ...

  9. ESP8266开发之旅 应用篇⑧Arduino版本 WiFi杀手

    文章目录 1. 前言 授人以鱼不如授人以渔,目的不是为了教会你具体项目开发,而是学会学习的能力.希望大家分享给你周边需要的朋友或者同学,说不定大神成长之路有博哥的奠基石... 共同学习成长QQ群 62 ...

最新文章

  1. Python基本语法_变量作用域LEGB
  2. 数据库及中间件术语解释
  3. 一个前端博客(9)——浏览器检测和加载
  4. 12月第2周业务风控关注 | 公安部:严打自媒体“网络水军”违法犯罪,关闭大V账号1100余个...
  5. Python 编写规范
  6. 科学道德与学风-2021雨课堂答案-第1章
  7. 图灵好书推荐——数学+物理+宇宙
  8. 浏览器 pad android,360安全浏览器平板电脑Pad专用版-360安全浏览器HD 安卓版v1.1.0-PC6安卓网...
  9. 解决拯救者Y7000打游戏,看视频没有声音的问题
  10. 重要文件即时搞定,不用插电就能打印,汉印MT800移动便携打印机上手
  11. 【用EXCEL编写俄罗斯方块小游戏(基于VBA)】
  12. 关于日记账导入-外币
  13. ios上传ipa:Xcode导入ipa上传至App Store
  14. [USACO 2010 Feb S]Chocolate Eating
  15. 美国签证(B1)经验总结
  16. JQuery 模糊匹配(JQuery 选择器模糊匹配、选择指定属性是以给定字符串开始的元素 )
  17. Cruzer Profile 原理分析
  18. Python对3D STEP/STP 文件解析
  19. linux运维工程师视频教程一(下)-张彬-专题视频课程
  20. html表白页面抖音,抖音表白代码

热门文章

  1. 竞拍商城APP开发有什么功能
  2. vc++ 2010错误 IntelliSense: 无法打开 源 文件 stdafx.h
  3. Oracle数据库将时间戳转换成年月日时分秒格式
  4. android 多套布局适配,Android屏幕适配 重点盘点
  5. 一天一点raknet_Editing 教程/WebSocket
  6. 数据库里怎么修改服务器爆率,关于数据库点窜爆率及点窜和增加掉落的教程(纯小白版)...
  7. kies air java 证书_Java ToStringBuilder類代碼示例
  8. c语言银行卡管理系统实验报告,C++编写的简单银行卡管理系统
  9. ffmpeg之demux 解复用
  10. 3a2b递归排列java,高考数学解题技巧-递推数列通项公式的十种策略例析