hOmewOrk 第三单元 总结

JML理论基础梳理

JML是用于对Java程序进行规格化设计的一种表示语言。

1. 注释结构

JML表示规格的内容包含在注释之中。可以使用行注释和块注释。行注释的表示方式为 //@annotation ，块注释的方式为 /* @ annotation @*/ 。

2. JML表达式

JML表达式是在基于JAVA语法基础上，新增了一些操作符和和原子表达式组成的。

2.1 原子表达式

\result表达式：表示方法执行后的返回值。

\old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值。

\not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。

\not_modified(x,y,...)表达式：与上面的\not_assigned表达式类似，该表达式限制括号中的变量在方法执行期间的取 值未发生变化。

\nonnullelements( container )表达式：表示 container 对象中存储的对象不会有 null。

\type(type)表达式：返回类型type对应的类型(Class）。

\typeof(expr)表达式：该表达式返回expr对应的准确类型。

2.2 量化表达式

\forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。

\exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。

\sum表达式：返回给定范围内的表达式的和。

\product表达式：返回给定范围内的表达式的连乘结果。

\max表达式：返回给定范围内的表达式的最大值。

\min表达式：返回给定范围内的表达式的最小值。

\num_of表达式：返回指定变量中满足相应条件的取值个数。

2.3 集合表达式

集合构造表达式：可以在JML规格中构造一个局部的集合（容器），明确集合中可以包含的元素。

2.4 操作符

(1) 子类型关系操作符： E1<:E2 ，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。

(2) 等价关系操作符： b_expr1<==>b_expr2 或者 b_expr1<=!=>b_expr2 ，其中b_expr1和b_expr2都是布尔表达 式，这两个表达式的意思是 b_expr1==b_expr2 或者 b_expr1!=b_expr2 。

(3) 推理操作符： b_expr1==>b_expr2 或者 b_expr2<==b_expr1 。对于表达式 b_expr1==>b_expr2 而言，当 b_expr1==false ，或者 b_expr1==true 且 b_expr2==true 时，整个表达式的值为 true

3. 方法规格

前置条件(pre-condition)：前置条件通过requires子句来表示： requires P; 。其中requires是JML关键词，表达的意思是“要求调用者确保P为 真”。

后置条件(post-condition)：后置条件通过ensures子句来表示： ensures P; 。其中ensures是JML关键词，表达的意思是“方法实现者确保方法执 行返回结果一定满足谓词P的要求，即确保P为真”。

副作用范围限定(side-effects):副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响。从方法 规格的角度，必须要明确给出副作用范围。

4. 类型规格

类型规格指针对Java程序中定义的数据类型所设计的限制规则。

不变式invariant：不变式（invariant）是要求在所有可见状态下都必须满足的特性。

状态变化约束constraint：对前序可见状态和当前可见状态的关系进行约束。

JML应用工具链

openJML

JUnit4

架构设计分析

第一次作业

原文地址：https://www.cnblogs.com/gagaein/p/10898938.html