1.JML基础梳理

1.1注释结构

JML采用javadoc注释的方式来表示规格，且每行以@开头。通过使用//@annotation来进行行注释，使用/*@annotaion@*/来进行块注释。

1.2JML表达式

1.2.1原子表达式

• \result表达式，在方法规格中使用，通过\result来指代返回值。在谓词中使用\result，来表达放回值的限制条件。

• \old(expr)表达式，返回表达式expr在方法执行之前的值。
• \not_assigned(x,y,...)表达式，该表达式为一谓词，当括号中变量在方法执行过程中未被赋值返回true，否则返回false。
• \not_modified(x,y,...)表达式，该表示为一谓词，当括号中变量在方法执行过程取值为变化返回true，否则返回false。

1.2.2量化表达式

• \forall表达式。表达式格式为\formall V; P1; P2。其中V定义了在该表达式中要使用的变量，谓词P1、P2为变量需要满足的条件。一般P1表示变量的范围，P2表示变量需要满足的其他条件。该表达式整体也为一个谓词，当V定义的变量的所有满足P1的取值都满足P2时返回true，否则返回false。
• \exists表达式。表达式格式为\exists V; P1; P2。其中V,P1,P2与\forall表达式中的相同。该表达式整体为一个谓词，当V定义的变量存在一个满足P1的取值也满足P2时返回true，否则返回false。
• \sum表达式。表达式格式为\sum V; P; N。其中V定义了表达式中要使用的变量，谓词P限制了变量的范围，N表示每一个满足P的情况下的增量。表达式最终返回所有增量的加和。

1.2.3操作符

• 推理操作符==>，使用格式P1 ==> P2。P1、P2为谓词，整个表达式也为一谓词。当P1为true，P2为false时该谓词返回false，否则返回true。
• 变量引用操作符。\nothing表示空集，\everything表示全集。

1.3数据规格

1.3.1规格变量

在本单元作业中，通过在接口中定义规格变量，来规定要管理的数据。

例如//@public instance model non_null int id；定义了一个规格可见的、引用不为空的、int型实例变量。同理将instance改为static可定义一个静态变量。

1.3.2 /*@spec_public@*/

通过对类中的字段添加/*@spec_public@*/可以指定该变量为规格可见。

1.1.3不变式invariant

//@invariant P；其中P为一个谓词。该语句规定在所有可见状态下，规格所管理的数据都必须满足谓词P。

1.1.4状态变化约束constraint

//@constraint P；其中P为一个谓词。该语句规定数据在前序可见状态与当前可见状态之间需要满足的约束。

1.4方法规格

1.4.1/*@pure@*/

通过对方法修饰/*@ pure @*/，表示该方法仅为查询方法，不会对类的数据做任何修改，使得该方法为规格内可见。

1.4.2行为

一个方法可以有多个行为，行为分为正常行为与异常行为。一个方法也也可以有多个正常行为与异常行为，但他们的前置条件之间不能有交集。正常行为用normal_behavior表示，异常行为用exceptional_behavior表示。多个行为之间用also连接。

1.4.3前置条件

通过使用requires语句实现。格式为requires P。P为一谓词，表示调用该方法时需要满足的限制。一个行为可以有多个requires语句，这些语句之间为且关系，在该行为下需全部被满足。

1.4.4后置条件

通过使用ensures语句实现。格式为ensures P。P为一谓词，表示该方法调用结束时需要满足的限制。一个行为可以有多个ensures语句，这些语句之间为且关系，在该行为下需全部被满足。

1.4.5副作用范围限定

通过assignable语句或者modifiable语句实现。格式为assignable/modifiable v。其中v表示可以被赋值/修改的变量。特别的，当v为\nothing时表示不能赋值\修改任何变量。

1.4.6 signals

signals语句使用在异常行为下。格式为signals E P。E为要抛出的异常包括异常类型与异常变量名称。P为一谓词，表示当谓词满足时抛出异常。当P与该行为前置条件的P相同时，可简化该语句为signals_only E。

2.工具链的具体使用

2.1 应用工具链情况

1. OpenJML：用于检查JML文档规格语法
2. JMLUnitNG：基于JML的单元测试工具，能够自动生成测试用例，注重边界条件的测试
3. Junit：单元测试，可用于编写和可重复运行的自动化测试。

2.2 OpenJML验证

::openjml.bat
@echo off

set java=java -jar "%~dp0openjml.jar" -noPurityCheck
set prove=-prover cvc4 -exec "%~dp0Solvers-windows\cvc4-1.6.exe"
set runtime=-cp %~dp0jmlruntime.jar;

set allparam=
set rac=

:param
set str=%1
if "%str%"=="" (
    goto end
)
if "%str%"=="-rac" (
	set rac=rac
)
if "%str%"=="-prove" (
	set str=%prove%
)
set allparam=%allparam% %str%
shift /0
goto param

:end
if "%allparam%"=="" (
    goto eof
)

rem remove left right blank
:intercept_left
if "%allparam:~0,1%"==" " set "allparam=%allparam:~1%"&goto intercept_left

:intercept_right
if "%allparam:~-1%"==" " set "allparam=%allparam:~0,-1%"&goto intercept_right

:eof
%java% %allparam%
set filename=
if "%rac%"=="rac" (
	:input
	set /p filename=Input file name:
	if "%filename%"=="" (
		goto input
	)
	java %runtime% %filename%
)


pause

将上述代码放在下载有JML的文件夹中，再将该文件夹加入环境变量。理论上就可以通过命令行使用openjml命令了。
查阅多处博客发现OpenJML的局限，比如规格不能存在exist,forall。

public class Test {
    /*@ public normal_behaviour
      @ ensures \result >= num1;
      @ ensures \result >= num2;
      @  \result >= num3;
    */
    public static int compare(int num1, int num2, int num3) {
        int max;
        if (num1 > num2) {
            max = num1;
        }
        else {
            max = num2;
        }
        if (max < num3) {
            max = num3;
        }
        return max;
    }

    public static void main(String[] args) {
        compare(347276,6234646, 2656435);
    }
}

以上使用openjml对代码进行检测

2.3 部署JMLUnitNG/JMLUnit

修改了MyGroup类，删除缓存的做法，去掉一些方法，仅为验证JMLUnitNG的功能

以上为使用junitng对代码进行检测。
查阅多处博客发现JMLUnitNG测试主要侧重于边界条件，比如对传入数据的可行域取边界进行测试。
这次测试主要依赖的还是数据生成器以及输出对拍来完成，有些规格或是测试规定的数据范围让这种测试方法更加便捷有效。而且本次作业针对一些代码实际实现可以手动构造一些特殊样例，来进行满载的测试。在类中的实现有时也不能完全按照JML规格完成，比如加入缓存之类的考量，这些使得类变为一个整体，不能单单测试某一个方法。

3.三次作业思路梳理

（由于此次的作业全部都是已知的思路，所以具体的思路以及算法实现等等方面在这里就省略了描写，只写这几次作业中本人出现的bug）

3.1 第一次作业的bug

由于第一次作业里面有一个深度优先搜索；然后听说“算法基本上不会在效率上卡大家”，而且听说这次作业没有优化分，所以就直接使用了最暴力的DFS深搜；不想最后却因为时间效率的问题被卡住了；看来最起码的优化还是要有的；

 3.2 第二次作业的bug分析

第二次作业的bug还是出在效率上；因为有一个查询算法使用了O(n2)的方法，而没有使用大家常使用的O(1)的方法，所以到最后效率上就差了很多很多；

 3.3 第三次作业的bug分析

由于第三次作业吸收了很多前两次的经验，所以就把大量的时间用来优化算法效率；无奈看错了数据范围，然后就对数据的整体特性有了错误的判断；然后就使用了一种在“我以为的数据范围”下效率会很高，但是在“真实数据范围”下效率超级低的算法；所以最后一次花了大量的时间做优化，但是最后还是效率出了问题；强测只过了几个点；偷鸡不成蚀把米，弄巧成拙；

4. 心得体会

这个单元看起来人畜无害，我却一次强测都没有进。综合来看，我自己也有一部分原因，但也并不是所有的问题都因为我。我得到了错误的传播信息，这导致了我第一次作业效率太低，最终被强测卡住；本地测试与评测机测试的某些差别，导致我第二次作业效率太低，最终被强测卡住；由于错误的理解的数据的范围，导致第三次作业失误，最终也被强测卡住；

虽然这个单元最简单，但是却是我写的最差的一个单元，主要是没有跟学长了解过相关的注意事项，而且跟同学的交流有点少，所以以后要注意从优质信息的来源方面入手来提高成绩，“卷”的精髓就在于找学长学姐 + 跟同学交流 + 提前做准备；

只要把这三点做好就能够拿到一个不错的成绩了吧。

BUAA_OO 第三单元总结

原文：https://www.cnblogs.com/alink61/p/12943900.html