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

OO第三单元总结

时间:2020-05-23 20:25:38      阅读:59      评论:0      收藏:0      [点我收藏+]

标签:图片   量化   ever   assigned   http   赋值   取值   arraylist   最大   

JML语言的理论基础、应用工具链

JML语言

JML是一种面向JAVA,形式化的行为接口规格语言。

JML表达式
  • 原子表达式
    \result:方法执行后的返回值
    \old(expr):一个表达式expr在相应方法执行前的取值
    \not_assigned(x,y):返回true表示括号中的变量在方法执行过程中没有被赋值,false则表示被赋值
    \not_modified(x,y):限制括号中的变量在方法执行期间取值不发生变化

  • 量化表达式
    \forall:全称量词修饰的表达式
    \exists:存在量词修饰的表达式
    \sum:返回给定范围内的表达式的和
    \max:返回给定范围内表达式的最大值
    \min:返回给定范围内表达式的最小值

  • 集合表达式
    实验和作业中还未应用到

  • 操作符
    \nothing:表示空集
    \everything:表示全集

方法规格
  • 前置条件requires P:表示调用者确保P为真
  • 后置条件ensure P:表示方法实现者确保执行返回后,确保P为真
  • 副作用范围限定assignablemodifiable:限定方法执行过程中修改对象的范围
  • 异常signals:抛出异常
类型规格
  • 不变式invariant:要求所有可见状态下都必须满足的特性
  • 状态变化约束constraint:对前序可见状态和当前可见状态的关系进行约束

工具链

  • OpenJML:检查JML语法的正确性
  • JMLUnitNG:自动化单元测试生成工具

架构设计

第一次作业

  • 第一次作业较为简单,理解了JML规格后基本不需要花太大功夫就能完成

第二次作业

  • 较第一次作业,JML复杂度提升,Person类变化不大,增加Group类,NetWork类稍有变化。不同于第一次作业,需要在算法上多做考虑。基础测试非常弱,自己也没有进行完整的测试,导致强测损失惨重。

第三次作业

  • 较第二次作业,Person类依旧基本不变,Group类增加删除功能,NetWork增加大量查询方法,稍不注意就会写出Bug或是超时。
    我牺牲了空间来换取时间,在Person类,Group类中使用ArrayList存person,HashMap存(id,listIndex)对,利用HashMap查询迅速的特性,稍稍降低查询时间。
    第二次作业中,找通路我使用了bfs的方法,并在第三次作业一开始,直接沿用到新增的方法中,但是对规格理解错误,导致产生bug。后来通过评论区交流贴,吸取大家经验,使用dijkstra来查询最短路径。
    技术图片

代码Bug

第三次作业中,在阅读最短路径的JML时,理解错误,没有用到边的权值,直接想当然把结点数作为路径长度,测试做得也不全面,导致强测出现bug。
在设计新增的几个方法时,没有想到好的方法,直接跟着JML写,出现了超时。目前正在bug修复。

心得体会

JML的出现大大方便了程序设计中,程序员对于需求的提取,一个优秀的规格能给我们提供很多便利。
同时,也更注重程序的复杂度,设计的时候,保证正确性的情况下,多对算法进行考虑。

OO第三单元总结

标签:图片   量化   ever   assigned   http   赋值   取值   arraylist   最大   

原文地址:https://www.cnblogs.com/5509spaceOfguozi/p/12943665.html

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