JML理论基础

• JML规定了一些语法,用这些语法可以描述一个方法,一个类的行为,理论基础是离散数学吧

JML常用语法

• 前置条件: 使用 require + 表达式 ,表达式一般为布尔表达式
• 副作用: assignable列出这个方法能够修改的类成员属性， othing是个关键词，表示这个方法不对任何成员属性进行修改，所以是一个pure方法。
• 后置条件: 使用 ensures + 表达式 , 表达式一般为布尔表达式.
• 常用语法:

  • 原子表达式:
    esult: 表示返回值.
    old(expr): 用来表示一个表达式expr在相应方法执行前的取值.
    ot_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。

  • 量化表达式(谓词逻辑):
    forall x;P(x);Q(x) ,对于所有的x,P(x)为真则Q(x)为真,
    exits x;P(x);Q(x),存在x,P(x)为真则Q(x)为真,
    sum i; 求和范围 ;累加值, 类似于数学中的求和
    prodoct i ;求积范围 ;累乘值, 类似于数学的求积

  • 集合表达式 没用到

  • 操作符: 等价 <==> 蕴含 ==>

  • 异常:
    public normal_behavior 正常行为
    public exceptional_behavior 要抛出异常的行为
    signals (***Exception e) b_expr; 当满足表达式时,抛出异常e
    signals_only Exception e 当满足前置条件时抛出异常e

  • 类型规格:
    invariant 可见状态下满足,可见状态一般指函数运行前后
    constraint 状态变化约束对前序可见状态和当前可见状态的关系进行约束

JML工具链

• OPENJML

  • OpenJML is a tool for working with logical annotations in Java programs. It enables static or run-time checking of the validity of the annotations, with other features underway.

  • 官方文档:http://www.openjml.org/documentation/execution.shtml

  • 失败案例
    

• JMLunitNG 自动生成测试用例

  • 官方文档 : http://insttech.secretninjaformalmethods.org/software/jmlunitng/usage.html
  • 失败案例:
    
    出现了警告和错误,找不到很好的解决方法.....

• 都跑不起来了,建议大佬写个教程....

模型分析

本单元的作业基本按照规格来实现即可,在模型构建上也没有过多的思考过.

bug和修复情况

• 第一次作业出现了没进互测的情况,一共出现了两个bug,其中一个是因为在修改checkstyle的时候删掉了一个空的if语句块,错了.另外一个是dfs写的复杂度太高了.
• 第二次作业无bug
• 第三次作业在求最短路径的时候又出现了tle的情况,基本是卡在了2秒多一点点,采用了堆优化加diji的算法,但是在实现上还是出了点问题,导致速度比别人慢了一秒多.bug修复时,疯狂修改代码的复杂度,最后发现是因为在network里面没有记录value导致了存取有一些时间上的差异.

规格撰写和理解

写规格真的不是一件容易的事情,感觉写规格要比写代码还要复杂,现实生活中应该不会有哪个团队写代码前先写一份规格吧.规格是站在更高的角度,使得对代码的测试更加遍历,那么你对规格的正确性的测试我自己感觉是远大于直接进行代码的测试,所以在这块感觉是很没有必要去搞这个规格的.如果规格就写错了,那实现者岂不是很尴尬.