标签：class 等价 条件 bool 指示 mlu require 努力 指定
JML的表达式是对Java表达式的扩展，新增了一些操作符和原子表达式。同样JML表达式中的操作符也有优先级的概念。
\result表达式：表示一个非void类型的方法执行所获得的结果，即方法执行后的返回值。
\old(expr)表达式：用来表示一个表达式expr在相应方法执行前的取值。该表达式涉及到评估expr中的对象是否发生变化，遵从Java的引用规则，即针对一个对象引用而言，只能判断引用本身是否发生变化，而不能判断引用所指向的对象实体内容是否发生变化。
\not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。如果没有被赋值，返回为true，否则返回false。
\not_modified(x,y,...)表达式：与上面的\not_assigned表达式类似，该表达式限制括号中的变量在方法执行期间的取值未发生变化。
\type(type)表达式：返回类型type对应的类型(Class)，如type(boolean)为Boolean.TYPE。TYPE是JML采用的缩略表示，等同于Java中的java.lang.Class。
\typeof(expr)表达式：该表达式返回expr对应的准确类型。如\typeof(false)为Boolean.TYPE。
\forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
\exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
\sum表达式：返回给定范围内的表达式的和。
\product表达式：返回给定范围内的表达式的连乘结果。
\max表达式：返回给定范围内的表达式的最大值。
\min表达式：返回给定范围内的表达式的最小值。
\num_of表达式：返回指定变量中满足相应条件的取值个数
集合构造表达式：可以在JML规格中构造一个局部的集合（容器），明确集合中可以包含的元素。
JML表达式中可以正常使用Java语言所定义的操作符，包括算术操作符、逻辑预算操作符等。此外，JML专门又定义了如下四类操作符。
(1) 子类型关系操作符：E1<:E2，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。
(2) 等价关系操作符：b_expr1<==>b_expr2或者b_expr1<=!=>b_expr2。
(3) 推理操作符：b_expr1>b_expr2或者b_expr2<b_expr1。
(4) 变量引用操作符：除了可以直接引用Java代码或者JML规格中定义的变量外，JML还提供了几个概括性的关键词来引用相关的变量。\nothing指示一个空集；\everything指示一个全集，即包括当前作用域下能够访问到的所有变量。
方法规格的核心内容包括三个方面，前置条件、后置条件和副作用约定。其中前置条件是对方法输入参数的限制，如果不满足前置条件，方法执行结果不可预测，或者说不保证方法执行结果的正确性；后置条件是对方法执行结果的限制，如果执行结果满足后置条件，则表示方法执行正确，否则执行错误。副作用指方法在执行过程中对输入对象或this对象进行了修改（对其成员变量进行了赋值，或者调用其修改方法）。
指针对Java程序中定义的数据类型所设计的限制规则，一般而言，就是指针对类或接口所设计的约束规则。从面向对象角度来看，类或接口包含数据成员和方法成员的声明及或实现。
抱歉，我又一次陷入了惯性，没有完成本单元的作业，下一单元我一定好好努力，想办法进入暑假的补修环节。
标签：class 等价 条件 bool 指示 mlu require 努力 指定
原文地址：https://www.cnblogs.com/rozyl/p/12941963.html
