标签:图片 量化 ever assigned http 赋值 取值 arraylist 最大
JML是一种面向JAVA,形式化的行为接口规格语言。
原子表达式
\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为真assignable
或modifiable
:限定方法执行过程中修改对象的范围signals
:抛出异常invariant
:要求所有可见状态下都必须满足的特性constraint
:对前序可见状态和当前可见状态的关系进行约束第三次作业中,在阅读最短路径的JML时,理解错误,没有用到边的权值,直接想当然把结点数作为路径长度,测试做得也不全面,导致强测出现bug。
在设计新增的几个方法时,没有想到好的方法,直接跟着JML写,出现了超时。目前正在bug修复。
JML的出现大大方便了程序设计中,程序员对于需求的提取,一个优秀的规格能给我们提供很多便利。
同时,也更注重程序的复杂度,设计的时候,保证正确性的情况下,多对算法进行考虑。
标签:图片 量化 ever assigned http 赋值 取值 arraylist 最大
原文地址:https://www.cnblogs.com/5509spaceOfguozi/p/12943665.html