一、JML语法总结

　　JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言。

　　一般而言，JML有两种主要的用法：
（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。

　　接下来对JML level 0，也就是最核心的部分做一下整理和归纳。

　　　　常见的JML语法：

原子表达式
esult	方法执行后的返回值
old(expr)	expr在方法执行前的取值
ot assigned(x,y...)	表示x, y在方法中未被赋值
ype(type)	返回值对应的类型
量化表达式
forall	全称量词
exists	存在量词
sum	表达式求和
product	表达式求累乘
max	给定范围内表达式的最大值
min	给定范围内表达式的最小值
um_of	指定变量中满足相应条件取值的个数
操作符
<:	子类操作符
<==>	等价关系操作符
==>	推理操作符
othing	空集
everything	全集
方法规格
equires	表示前置条件
ensures	表示后置条件
assignable	副作用限定

二、关于利用SMT Solver的验证

　　本人以命令行的方式使用SMT Solver对较为简单的Person类（为进行测试以进行修改）进行了静态检查。

　　OpenJML指路：JML工具链、OpenJML下载

　　运行命令：

java -jar openjml.jar -exec z3-4.7.1.exe -esc Person.java

　　得到结果如下：

　　出现的警告，多是因为OpenJML工具本身的问题造成的。

　　OpenJML本身并不完善，而且这个项目已经很久没有更新了，有很多复杂一些的JML逻辑都无法予以支持，可以说十分的鸡肋。使用OpenJML在笔者看来还不如和小伙伴用肉眼检查代码来的效率高。

三、使用JMLUnitNG进行测试

　　JMLUnitNG指路：JMLUnitNG下载

　　JMLUnitNG号称可以根据自动生成测试用例进行方法测试，感觉很niupi那么让我们看看效果。

　　下载1.4版本jar包后，使用如下命令：

java -jar jmlunitng.jar test/Group.java

javac -cp jmlunitng.jar test/*.java

java -jar openjml.jar -rac test/Group.java test/Person.java

java -cp jmlunitng.jar test.Group_JML_Test

　　得到测试结果如下：

　　乍一看感觉还不错，但是再看一个Demo：

public class Demo {
    
    /* @ public normal_behavior
     * @ ensures 
esult == (a + b);
     */
    public int aAddb(int a, int b) {
        return a + b;
    }
 
    /* @ public normal_behavior
     * @ ensures 
esult.equals(s);
     */
    public/*@ pure @*/ String getString(String s) {
        return s;
    }
    
}

　　对于这个Demo的测试效果如下：

　　可以看出这个JMLUnitNG生成的测试用例就是传几个参数，对于int类型就传入INT_MIN、0、INT_MAX，对于引用类型就干脆传null。实际应用价值几乎为零（测这东西我为什么不用JUnit呢？）

四、作业设计

　　第一次作业：

　　先放上UML图：

　　本次作业是第三单元第一次作业，主要目的是了解如何使用JML描述规格以及如何根据规格来写代码。本次作业唯一的难点在于isCircle函数，这个函数的作用是判断图中两点的可达性。由于我DS基础打得不牢固以至于将dfs写错了，以及本地测试做得不足再加上自己内心上对于第三单元的轻视。就很自然的翻车了，未能进入互测，这也让我痛定思痛决心痛改前非。

　　第二次作业：

　　先上UML图：

　　本次作业是第三单元第二次作业，相比于第一次作业增加了group类和相应的方法，总体上难度不大。但需要注意方法的复杂度，不然会翻车。我在本次作业的queryGroupRelationSum和queryGroupValueSum方法中使用了双循环，这O(n^2)的复杂度直接让我上天，不过好在只有这一个问题，在强测中只错了一个点。在之后的bug修复阶段我选择使用一个变量来存放两个sum值，在addperson或者addrelation时进行更新，查询时仅需return这两个sum即可。值得一提的是在本次作业中为了避免上一次作业中的问题，我将isCircle方法从dfs改成了bfs。

　　这次作业让我深刻理解了JML代表的契约式设计只关心条件和结果，对于实现，如果照搬jml的描述，绝对是不可取的。

　　第三次作业：

　　UML类图：

　　本次作业相比与上次作业又增加了一些方法，主要需求是，查询两个点间的最短路径，查询图中的连通块数以及查询两个点是否存在两条无相同点的路径。在本次作业中我采用了堆优化（使用优先队列）的迪杰斯特拉算法、并查集算法和bfs算法。在进行本次作业的过程中，我充分吸取了上两次作业中的教训，不放弃任何可以优化的地方，并且做足了测试。在强测和互测中均未发现bug。

五、关于Bug的测试

　　以第三次作业的bug测试为例，我使用了python生成测试数据，shell进行对拍的策略，效果非常不错，在作业自我测试过程中，发现了不少bug。但是也有不足之处，例如本地测试对于运行时间和cpu时间的把握不准确，对拍双方的共性问题难以发现等，对于互测，别人不刀我我也懒得刀别人了，善良一些吧hhhhh

　　附上测试代码：

python:

  1 from random import choice, randint
  2 from xeger import Xeger
  3 limit = 20
  4 time_all = 50
  5 time_ap = 800
  6 time_ag = 10
  7 time_qsl = 20
  8 time_qnr = 1000
  9 max_age = 2000
 10 max_value = 1000
 11 regex_name = r'[a-z]{1,10}'
 12 regex_char = r'[1-9][0-9]{10,18}'
 13 x = Xeger(limit)
 14 t_ap, t_qsl, t_ag, t_qnr = 0, 0, 0, 0
 15 inst_list_a1 = [
 16     (0, "ap", " {0} {1} {2} {3}", "id_p", "name", "char", "age"),
 17     (1, "ar", " {0} {1} {2}", "id_p", "id_p", "value"),
 18     (0, "ag", " {0}", "id_g")
 19 ]
 20 inst_list_a2 = [
 21     (1, "atg", " {0} {1}", "id_p", "id_g"),
 22     (1, "atg", " {0} {1}", "id_p", "id_g"),
 23     (1, "atg", " {0} {1}", "id_p", "id_g"),
 24     (1, "atg", " {0} {1}", "id_p", "id_g"),
 25     (1, "dfg", " {0} {1}", "id_p", "id_g")
 26 ]
 27 inst_list_q_p = [
 28     (1, "qv", " {0} {1}", "id_p", "id_p"),
 29     (1, "qc", " {0} {1}", "id_p", "id_p"),
 30     (1, "qas", " {0}", "id_p"),
 31     (1, "ca", " {0} {1}", "id_p", "id_p"),
 32     (1, "cn", " {0} {1}", "id_p", "id_p"),
 33     (1, "qnr", " {0}", "id_p"),
 34     (1, "qps", ""),
 35     (1, "qci", " {0} {1}", "id_p", "id_p"),
 36     (1, "qasu", " {0} {1}", "age", "age"),
 37     (1, "qmp", " {0} {1}", "id_p", "id_p"),
 38     (1, "qsl", " {0} {1}", "id_p", "id_p"),
 39     (1, "qbs", ""),
 40     (1, "bf", " {0} {1} {2}", "id_p", "id_p", "value"),
 41     (1, "qm", " {0}", "id_p")
 42 ]
 43 inst_list_q_g = [
 44     (1, "qgs", ""),
 45     (1, "qgps", " {0}", "id_g"),
 46     (1, "qgrs", " {0}", "id_g"),
 47     (1, "qgvs", " {0}", "id_g"),
 48     (1, "qgcs", " {0}", "id_g"),
 49     (1, "qgam", " {0}", "id_g"),
 50     (1, "qgav", " {0}", "id_g")
 51 ]
 52 inst_list = [
 53     inst_list_a1, inst_list_a2, inst_list_q_p, inst_list_q_g
 54 ]
 55 people_set = []
 56 groups_set = []
 57 
 58 
 59 def get_id(set_list):
 60     i = randint(1, 10000)
 61     while set_list.__contains__(i):
 62         i = randint(1, 10000)
 63     return i
 64 
 65 
 66 rand_func = [
 67     {
 68         'id_p': lambda line: get_id(people_set),
 69         'id_g': lambda line: get_id(groups_set),
 70         'name': lambda line: x.xeger(regex_name),
 71         'char': lambda line: x.xeger(regex_char),
 72         'age': lambda line: randint(0, max_age),
 73         'value': lambda line: randint(0, max_value)
 74     },
 75     {
 76         'id_p': lambda line: choice(people_set) if (len(people_set) > 0) else randint(0, 10000),
 77         'id_g': lambda line: choice(groups_set) if (len(groups_set) > 0) else randint(0, 10000),
 78         'name': lambda line: x.xeger(regex_name),
 79         'char': lambda line: x.xeger(regex_char),
 80         'age': lambda line: randint(0, max_age),
 81         'value': lambda line: randint(0, max_value)
 82     }
 83 ]
 84 
 85 
 86 def test_qp(i):
 87     if i < time_all * 0.3:
 88         return 0
 89     if i < time_all * 0.5:
 90         return 2
 91     if i < time_all * 0.7:
 92         return 0
 93     return 2
 94 
 95 
 96 def test_qg(i):
 97     if i < time_all * 0.3:
 98         return 0
 99     if i < time_all * 0.5:
100         return 1
101     if i < time_all * 0.6:
102         return 3
103     if i < time_all * 0.8:
104         return 1
105     return 3
106 
107 
108 def test_rand_qg(i):
109     if i < 500:
110         return 0
111     if i < 700:
112         return 1
113     return choice([1, 3])
114 
115 
116 def test_rand_qp(i):
117     if i < 500:
118         return 0
119     return choice([0, 2])
120 
121 
122 def test_rand(i):
123     if i < 1000:
124         return randint(0, 1)
125     return randint(0, 3)
126 
127 
128 def judge_time(inst):
129     global t_ap, t_ag, t_qnr, t_qsl
130     if inst == 'ap':
131         if t_ap < time_ap:
132             t_ap += 1
133             return True
134     elif inst == 'ag':
135         if t_ag < time_ag:
136             t_ag += 1
137             return True
138     elif inst == 'qnr':
139         if t_qnr < time_qnr:
140             t_qnr += 1
141             return True
142     elif inst == 'qsl':
143         if t_qsl < time_qsl:
144             t_qsl += 1
145             return True
146     else:
147         return True
148     return False
149 
150 
151 def get_test():
152     f = open("input.txt", "w")
153     for i in range(time_all):
154         inst_kind = test_qp(i)
155         u = choice(inst_list[inst_kind])
156         while not judge_time(u[1]):
157             u = choice(inst_list[inst_kind])
158         kind, inst, pos, arg = u[0], u[1], u[2], u[3:]
159         # kind = randint(0, 4)
160         # if kind != 0:
161         #     kind = 1
162         inst = inst + pos.format(*map(lambda x: rand_func[kind][x](i), arg))
163         s = inst.split(' ')
164         if s[0] == 'ap':
165             people_set.append(int(s[1]))
166         elif s[0] == 'ag':
167             groups_set.append(int(s[1]))
168         f.write(inst + '
')
169 
170 
171 if __name__ == '__main__':
172     get_test()

View Code

shell：

 1 #! /bin/bash
 2 mode=0
 3 time=100
 4 if [ $mode -eq 1 ]; then
 5     time=1
 6 fi
 7 i=0
 8 TMOUT=3
 9 while [ $i -lt $time ]
10 do
11     echo "Begin ${i}th test"
12     echo "Getting Input"
13     if [ $mode -eq 0 ];then
14         python get_input.py
15     fi
16     echo "Running *.jar"
17     (time java -jar p11_1.jar<input.txt>output.txt) 2>time_1.txt
18     t=$(grep -o "[0-9]+.[0-9]+" time_1.txt | sed -n '1p' | awk '{print int($0)}')
19     if [ $t -gt $TMOUT ];then
20         echo "TIMEOUT!!!(you)"
21         break
22     fi
23     (time java -jar p11_2.jar<input.txt>output_crz.txt) 2>time_2.txt
24     t=$(grep -o "[0-9]+.[0-9]+" time_2.txt | sed -n '1p' | awk '{print int($0)}')
25     if [ $t -gt $TMOUT ];then
26         echo "TIMEOUT!!!(crz)"
27         break
28     fi
29     echo "Compare"
30     diff -c output.txt output_crz.txt > diff.txt
31     if [ $? != 0 ];then
32         echo "DIFFER!!!"
33         break 
34     fi
35     echo "Over"
36     echo "-----------------------------"
37     ((i++))
38 done

View Code

六、心得体会

　　虽然我本单元开门红，但是本单元的三次作业真的不难（相比而言倒是本单元的两次实验比较hhh）。我想本单元的目的是为了让大家了解契约式设计的理念，这样的设计理念理论上来说的确可以让开发协同变得更为高效，用规格来约束设计也的确可以使设计更为规范减少bug。但是就我个人对于JML使用的体验来说，JML对于我真的没有什么帮助，一方面，没有成熟的工具链，使用起来十分别扭；另一方面，JML语言虽然做到精准的形式化描述，但它本身写起来极为繁琐且可读性差，如果一个工具不能带来实质上的生产力提升确非要使用，在我看来大可不必。从另一个角度上来说，有需求才有市场，JML工具链的不完善，我认为有JML本身易用性差的一部分责任。不好用的东西用的人就少，用的人少开发者就没有动力为它开发工具。但是经过这一单元的学习，我也认为规格本身是及其有必要的，如果规格描述得好可以减少很多不比要的麻烦，但我认为规格本身并不一定要完全用形式化描述，使用自然语言对需求和约束进行描述，在容易产生二义性的地方用形式化语言进行规范应当能更好地提升效率。