PDF《JML(Level 0)使用手册》

false 表示不相等). \old( expr )表达式:用来表示一个表达式 expr 在相应方法执行前的取值.该表达式涉及到评估 expr 中的对象是否 发生变化,遵从Java的引用规则,即针对一个对象引用而言,只能判断引用本身是否发生变化,而不能判断引用所指 向的对象实体内容是否发生变化.假设一个类有属性 v 为HashMap ,假设在方法执行前v的取值为 0x952ab340 ,即 指向了存储在该地址的具体 HashMap 对象,则\old( v )的值就是这个引用地址.如果方法执行过程中没有改变 v 指向 的对象,则v和old( v )有相同的取值,即便方法在执行过程中对 v 指向的 HashMap 执行了插入或删除操作.因此 v.size() 和\old( v ). size() 也有相同的结果.很多情况下,我们希望获得 v 在方法执行前所管理的对象个数,这 时应使用\old( v.size() ).作为一般规则,任何情况下,都应该使用\old把关心的表达式取值整体括起来. \not_assigned(x,y,...)表达式:用来表示括号中的变量是否在方法执行过程中被赋值.如果没有被赋值,返回为 true ,否则返回 false .实际上,该表达式主要用于后置条件的约束表示上,即限制一个方法的实现不能对列表中 的变量进行赋值. \not_modi?ed(x,y,...)表达式:与上面的\not_assigned表达式类似,该表达式限制括号中的变量在方法执行期间的取 值未发生变化. \nonnullelements( container )表达式:表示 container 对象中存储的对象不会有 null ,等价于下面的断言,其中 \forall是JML的关键词,表示针对所有 i . \type(type)表达式:返回类型type对应的类型(Class),如type( boolean )为Boolean.TYPE.TYPE是JML采用的缩略 表示,等同于Java中的 java.lang.Class . \typeof(expr)表达式:该表达式返回expr对应的准确类型.如\typeof( false )为Boolean.TYPE. 2.2 量化表达式 \forall表达式:全称量词修饰的表达式,表示对于给定范围内的元素,每个元素都满足相应的约束. (\forall int i,j;

0