OO第三单元总结——JML

Posted liuqian9961

tags:

篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了OO第三单元总结——JML相关的知识,希望对你有一定的参考价值。

JML理论

jml是对java程序进行规格化设计的一种表示语言。jml主要运用在:(1)开展规格化设计;(2)针对已有的代码书写规格,增强代码的可维护性。

需要注意的是:jml描述的是我们的程序在什么样的情况下会正确执行,预期的返回值满足什么样的条件,一言以蔽之:jml描述的是程序能用什么样的原料做出什么样的菜,而不是告诉你如何做菜。这一点也是笔者犯过的典型错误。

接下就对jml中常见的表达式进行总结:

esult 表示一个返回值不为void的方法执行后的返回值。

old(expr) 表示一个表达式expr在相应方法执行之前的取值。

ot_assigned(x,y,...) 表示括号中的变量在执行过程中是否被赋值,但是在实际使用中常常在后置条件中对括号中的变量进行约束,即限制方法对括号中的变量进行修改。

forall 全称量词,实际使用和for循环类似(forall xx ; xx ; xx)

exists 存在量词,实际使用forall类似

sum 返回给定范围内表达式的和。(sum int i ; 0 <= i && i <= 5 ; i),结果就是15

product 返回给定范围内表达式连乘的积,使用和sum类似。

max && min 返回给定范围内表达式的最大(最小)值。

requires 方法的前置条件,只有满足前置条件的情况下方法才能被正确执行,因此调用者需要确保前置条件为真。

ensures 方法的后置条件,方法保证执行完毕后的结果满足后置条件的约束。

assignable 副作用限定,即方法在执行过程中允许或者可能对某些变量进行修改。

signals 抛出相应的异常。

JML工具链

solver

技术图片

在运行solver后出现了如上的警告信息,核对后发现警告信息提示我了运算有可能存在溢出的情况。

jmlunitng

技术图片

 

 技术图片

 

 

分析结果后发现失败的情况分别为计算结果溢出和传入参数为 null的情况。对于计算溢出,我认为在实际中这是很有可能发生的,确实应该加以考虑,在出现这种情况时应该抛出对应的异常。参数为空的情况也应该进行一定的考虑,比如如果为空就直接返回,这样就能解决这一问题。

架构设计

在本系列作业中,笔者采用的架构直接简单接用了所给接口的架构,即:MyNetwork、MyPerson、MyGroup的形式。MyNetwork中管理的是整个社交网络的所有人员以及小组情况,MyPerson管理的是某一个特定的人的基本资料以及社交关系,MyGroup管理的是某一小组的成员情况以及小组成员间的关系。但是实际上这样的架构并不理想(这部分在BUG分析中会详细分析)。

技术图片

 

 

以上是本人的类图,虽然看起来还是比较对称美观的,但是由于架构的不合理,在某些方法的实现上就出现了比较大的问题。

BUG分析

第一次作业

没有出现BUG。

第二次作业

出现部分CTLE的BUG。第二次作业中主要的问题是出现了大量的查询方法,在笔者编写程序的时候,只是机械的翻译了JML并没有想到对方法进行一定的优化,导致每一次查询操作都需要进行遍历,时间复杂度极高。在出现BUG后,笔者针对此问题进行了修改,其实也很容易,只要增加相应的中间变量,在添加person或者relation的时候对中间变量进行维护,这个问题就很好的得到了解决。

第三次作业

出现部分CTLE的BUG。在仔细对数据进行分析后,笔者发现主要的问题出现在qmp方法上,最初笔者采用的是最朴素的Dijkstra算法,存在的问题还是在于复杂度过高。在与同学进行讨论后,我决定采用优先队列的Dijkstra算法进行优化。借助优先队列的优点在于每次查询最短边的操作只需要O(1)的复杂度。但是查询边的时候,需要的是与起点临接的边的情况,而不是点的情况。但是在笔者原有的架构中只记录了点的情况,这就是架构分析中提到的不合理之处。因此,笔者对架构进行了修改,增加了Edge类,存储的是两点间边的情况,同时在MyPerson中也增加了对所有关系的边的情况进行存储的变量。优化后的类图如下:

技术图片

 

 

在优化完成后,程序的cpu时间降低了一半之多,充分体现了合理架构的价值。

心得体会

本系列作业是笔者第一次接触JML,在学习过程中才了不少坑,但是也有很多的收获。笔者印象最深刻的就是JML描述的是方法的规格而不是方法的实现。在第一二次作业中,笔者就陷入了机械翻译JML规格的误区,导致一些很常见的优化方法都没有采用,反而保留了暴力的方法,使得程序的性能并不理想。其次,架构的设计也重要,比如这系列作业实际上就是图,那么采取什么样的形式存储就是一个问题。从需求来看,时间在作业中比存储空间更重要,在这样的情况下可以适当的牺牲空间换取时间,根据需要把需要的信息都存储一遍,减少查询操作的复杂度就是很好的思路。经过本次作业,笔者也充分体会到了JML的用处以及JML的正确打开方式。规格化的描述对于工程开发有很多的好处,在接下的笔者也会尝试着在自己的程序中采取这样的方法进行描述,更加规范的开发。

 

以上是关于OO第三单元总结——JML的主要内容,如果未能解决你的问题,请参考以下文章

OO第三单元总结规格JML和社交关系系统

oo第三单元总结

OO第三单元总结

OO第三单元总结——JML

OO第三单元总结

OO第三单元——基于JML的社交网络总结