1.JML语言的理论基础和应用工具链情况

1）概述

JML是一种行为接口规范语言，其体现的是一种契约方法设计，也即在声明方法的时候，对输入和输出进行了一些规定，而从形式上jml是以javadoc注释的方式来写的，也即在注释块中每行的开头都是@。

2）结构

一段完整的JML，往往有如下几个结构requires（前置条件）、ensures（后置条件）、assignable（副作用）、signals（抛出异常）。

以下面这段代码为例

/*@ public normal_behavior
      @ requires containsPathId(pathId);
      @ assignable \nothing;
      @ ensures (\exists int i; 0 <= i && i < pList.length; pidList[i] == pathId && \result == pList[i]);
      @ also
      @ public exceptional_behavior
      @ requires !containsPathId(pathId);
      @ assignable \nothing;
      @ signals_only PathIdNotFoundException;
      @*/
    public /*@pure@*/ Path getPathById(int pathId) throws PathIdNotFoundException;
  //取自PathContainer.java

其表示normal behavior需要满足包含这个pathid，同时该方法不应修改任何对象的属性数据或者类的静态成员变量。在满足normal behavior的要求的时候，应该确保返回结果等于是否造pidlist中有一个元素等于我们传进来的pathid。否则当不包含这个pathid的时候返回PathIdNotFoundException（事实上signals后面也可以加条件，表示满足何种条件抛出何种异常。normal和exceptional的requires不能有所重合。

额外在这里提一句，诸如下面这种情况，elements不一定要限制于如下的定义，甚至在实现时不必提供这样的定义，而仅仅是对问题的一种描述。

//@ public model non_null int [] elements

3）表达式

这一部分都是我们学过的一些定义什么的感觉没有什么意思，就简单了列举了一下在我们 的作业和实验中使用的过的表达式了。

原子表达式：

\result : 方法的返回值

\old(expr) : 表达式在执行该方法前的值

量化表达式：

\forall:

(\forall int i,j; 0 <= i && i < j && j < 10; a[i] < a[j])

表示任意一对ij，只要满足0 <= i && i < j && j，就有a[i] < a[j]

\exists:

(\exists int i; 0 <= i && i < 10; a[i] < 0)

表示存在i，在0 <= i && i < 10范围上，满足a[i] < 0

 

//集合表达式和操作符我是真的没见过Orz

 

其他：

pure:表示纯方法，就是不会动那些成员变量等等blabla的。

public_spec:这个变量或者方法是公开的

invariant:不变量

not_null:非空

4）工具链

JMLUnitng：用于自动生成测试用例

OpenJml：检查代码是否符合JML规定的规格

SMT Solver：形式化验证

2.部署JMLUnitng//JMLUnit

//全程就靠巨佬们（尤其是讨论区的某伦佬）带我飞了Orz

1）安装

jmlunitng的jat包下载链接（来自伦佬）：

http://insttech.secretninjaformalmethods.org/software/jmlunitng/assets/jmlunitng.jar

//好东西要向更多的人分享QAQ

其实没有安装后这个环节，把这个jar包和待测文件放在一起（其实也可以不在一起但是我 懒惰了）就可以，使用的时候直接

java -jar xxx/jmlunitng.jar yyy.java

就可以。其中xxx为jar包的路径，我放在一起了，所以就没有，yyy就是待测文件

2）生成测试

这真的可以嘛。。。它显示满屏的这个玩意，大概是这个文件用到了其他文件以及其他jar 包里面定义的东西，它生成的时候找不到定义了吧Orz。

 

这个时候就只能随便手写一个样例文件的了Orz。

然后又遇到了一系列错误，当时因为咱也不知道，咱也不敢问，所以没记录下来，也没进一步做实验验证，此处就省略了,不过基本上都是老老实实按照讨论区巨佬们讲的走就能走的通的。只有几个我印象比较深的无聊琐碎但搞得人神烦的，一个是jmlunitng.jar好像不能和文件放在一个package里面，必须和package并列，还有一个是我手搓代码的jml的时候忘了加pidlist的声明，以及改成static了，以及运行的时候我忘了把/改成.，等等手残智障的错误。Orz

 

 

 

3.代码架构

这一块几乎没有什么，前两次几乎就是指导书要求了什么文件就老老实实按照那个文件写，除了定义无序偶什么的。然后每次作业都是完全继承上一次作业的，所以感觉也没什么可说的。最后一次我基本上还是按照指导书来的，就是models里面基本上就是指导书里面提到的，function里面是四种新功能，还有ds里面是新定义的edge,<node,path>偶对np，newedge:<np,np>偶对，以及distancenp<distance,newedge>偶对等。

 

每次作业都只完成了新的功能，对原功能就是完全的继承，但是总体上代码的架构非常的不好，比如没有把一些数据结构及其计算单独提取出来作为一个类（比如标程的图），造成了重用性很差，维护起来也不太好维护，扩展就是直接的堆Orz，这一块算法太差所以光注重算法了，架构又被我抛在了脑后，每次作业我都得重写好几遍，既因为代码架构不好造成重写的更加麻烦，也因为不断的重写造成架构的混乱，总之感觉写的愧对这快一个学期的OO了/xk。Orz

第三次作业架构

 

第一、二次作业架构（第一次合并在第二次中了）因为重写次数过多，造成有的类没有用到。container里面就是一个简单的graph继承path_container。

4.bug情况

第二次作业有一个bug，确实可以用jml的规格检查出来的错误，当时没弄，对拍的次数也比较少造成的错误，很容易就修改了。

第二次TLE了好多点Orz，在之前的大量对拍中已经发现T的问题了，不过我虽然写了三个版本的查询，但是只有这个版本拍的比较充分，而我以为最多挂2-3个点，我本着怕wa的原则就懒得改了，结果，，，就T了，于是重写用了之前的一个版本。。。

5.心得总结

jml我第一次认真读了，第二次我只在debug时读了，第三次我确实没读，主要是算法知识比较贫瘠，对各个数据结构和算法的效果也没有什么掌握，所以对怎么实现共最好几乎占了我绝大部分的时间和经历，不过实践出真知，在算法之间、数据结构之间的实现是的时间和空间的复杂度的掌握特别是判断的方法论都有所提升，不过遗憾的是jml确实读的不多，用的不多，写的就更不多了，主要还是一个入门了解和认识的作用，也确实能让人学到新东西，在工程实践中能开阔一下眼界。