第三单元总结

系统管理员 2021-12-24 09:21 204阅读 0赞

# 第三单元总结 #

## JML相关 ##

### 一 梳理JML语言的理论基础、应用工具链情况 ###

*  JML是一种形式化的, 面向JAVA的行为接口规格语言( behavioral interface specification language) JML允许在规格中混合使用Java语法成分和JML引入的语法成分. JML主要是实现了设计与实现相分离, 使得设计时不会陷入实现的困难中去. 实现时, 由于JML实现已经设计完整, 也不必担忧设计上的缺陷.
 *  JML相关的工具主要有OpenJML和JMLUnitNG, 前者类似于一个编译器, 主要用来检查JML语法的正确性. 后者主要用于根据JML对给定的单元进行测试.

### 二 部署SMT Solver，至少选择3个主要方法来尝试进行验证，报告结果( 有可能要补充JML规格) ###

*  最新版作业已取消该部分

### 三 选择相关的简单方法，自己补充规格，确保未使用\\exists或\\forall表达式，使用jmlunit或jmlunitng来生成测试数据，并分析所生成数据的特点。 ###

*  使用的代码:
    
    test/Test.java:
    
        package test; public class Test { /*@ public normal_behaviour @ ensures \result == va + vb; */ public static int add(int va, int vb) { return va + vb; } public static void main(String[] args) { add(1000,2000); return ; } }
 *  结果:

![1270250-20190522154231708-364287924.png][]

*  分析:
    
    从上面的生成样例可以看到, 其自动生成的样例基本上就是临界数据, int类型的边界值, 以及0, null等.

### 四 按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构 ###

*  有了JML规格指引, 在后续开发中, 相对前两个单元的重构代码量, 重构难度等都显著降低, 可以看到JML是个好东西, 我们应该多多应用.
 *  第一次作业采用了两个HashMap来存储Path和PathId的一一对应关系, 这种解决办法很好. 但由于要用Path做HashMap的Key, 所有需要重写其HashCode方法.
 *  第二次作业增添了最短路径查询, 采用了简单好用的Floyd算法, Floyd算法也不负所托, 完美完成任务.
 *  第三次作业开始并不会写, 主要参考了讨论区wjy同学的算法( 称其为wjy算法) , 该算法虽然表面上看起来复杂度很高, 但实测结果( 强测100) 表明并不是那么回事, 采用了wjy算法之后也并没有对原有的架构产生冲突, 只是增加了几个建图模型.

### 五 按照作业分析代码实现的bug和修复情况 ###

*  第一次作业一开始没有使用双Map方式, 导致查询超时, 后来使用了双Map方式, 解决了该问题.
 *  第二次作业出了一个小bug, 求自圈的最短路径出现了问题, 有可能会算出1, 后来修改了Floyd算法的具体实现修复了该Bug.
 *  第三次作业由于采用了先进的wjy算法, 并未出现任何bug.

### 六 阐述对规格撰写和理解上的心得体会 ###

*  规格这个东西, 自我感觉更像是数学, 而不是计算机的东西, 要求在形式上描述所需. 类似于谓词逻辑体系.
 *  使用了规格之后, 能够更为精确地描述这些代码是做什么的.
 *  能够更方便地写成测试程序, 同时也能够高效地发现和修正程序中的 bug, 还可以在应用程序升级时降低引入 bug 的机会
 *  规格既可以直到编写代码的人, 反过来也可以成为程序的说明文档, 其描述比自然语言更贴近程序的功能.

转载于:https://www.cnblogs.com/black-watch/p/10902201.html

[1270250-20190522154231708-364287924.png]: /images/20211223/19a5754b1636469f9acb027d8f87e97e.png