BUAA_OO_JML

(1)梳理JML语言的理论基础、应用工具链情况

Java建模语言(JML)是一种行为接口规范语言,可用于指定Java模块的行为 。它结合了Eiffel的契约方法设计 和Larch系列接口规范语言的基于模型的规范方法 ,以及细化演算一些元素 。

JML有标准的注释结构,由JML的语法表达式构成,有固定的方法规格和类型规格。

JML应用工具链

openjml是所有工具链的核心,可以通过命令行工具对代码进行jml的语法检查,代码静态推导和动态检查。

在eclipse中,有jml的官方gui,但是仍然是基于openjml命令行的,命令行有的问题gui里一应俱全,不过gui中可以更有针对性的给出一部分推导过程,使用起来很方便。

jmlunitNG则是一个根据testNG进行测试,能根据jml来生成测试样例的工具。

• (2)【改为选做,能较为完善地完成的将酌情加分】部署SMT Solver,至少选择3个主要方法来尝试进行验证,报告结果

 (3)部署JMLUnitNG/JMLUnit,针对Graph接口的实现自动生成测试用例(简单方法即可,如果依然存在困难的话尽力而为即可,具体见更新通告帖), 并结合规格对生成的测试用例和数据进行简要分析

测试样例

BUAA_OO_JML

测试结果

BUAA_OO_JML

 

• (4)按照作业梳理自己的架构设计,并特别分析迭代中对架构的重构

三次作业类图

BUAA_OO_JML

BUAA_OO_JML

BUAA_OO_JML

第一次采用hashmap以pair<>为key存储边,value存储边的个数,同样点也这样存储。

对于removebyid和removebypath,采用双向hashmap,path为key存储边,value存储边的值,另一个反之

第二次加入了图

用佛洛依德算法,利用边集重构

每次加入和删除操作重新构建最短路径

第三次综合了地铁路线

我们构建不同的图,最短路径,最低价格,最低满意度,构建不同的权重图,但是用一样的迪杰斯特拉算法

对于换乘采用了拆点算法

• (5)按照作业分析代码实现的bug和修复情况

第二次的用PAIR导致cpu超时,用简单的数组矩阵会提高更多的效率

• (6)阐述对规格撰写和理解上的心得体会

感觉JML规格能很好的规定数据的改变,和算法的约定。

上一篇:CSS实现限制显示的字数,超出显示"..."


下一篇:【BUAA-OO】第四单元作业总结