码迷,mamicode.com
首页 > 其他好文 > 详细

OO第三单元总结——JML

时间:2020-05-23 11:12:06      阅读:40      评论:0      收藏:0      [点我收藏+]

标签:max   focus   结果   比较   image   png   运算   返回值   中间   

JML理论

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

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

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

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

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

\not_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

标签:max   focus   结果   比较   image   png   运算   返回值   中间   

原文地址:https://www.cnblogs.com/liuqian9961/p/12941496.html

(0)
(0)
   
举报
评论 一句话评论(0
登录后才能评论!
© 2014 mamicode.com 版权所有  联系我们:gaon5@hotmail.com
迷上了代码!