OO第三单元作业(JML)总结
一：梳理JML语言的理论基础，应用工具链情况
对于JML(Java Modeling Language)是对java的一种建模语言，通过JML可以规定不同方法，不同类希望完成的动作与行为，对整个开发过程有着良好的监控行为。该建模语言在以注释的形式内嵌在代码中，它对代码对对象的修改、以及返回值、异常情况的抛出等等进行了限制，但对算法的实现层面确实放松的。
JML能够约束整个代码结果，但是JML的限制先决条件是该JML的正确性，只有一个正确的JML，才能够引导正确的结果。并且JML这种对结果进行规定，而不规定过程的语言，更适合于形成测试，可以针对JML的描述，针对性的构造测试样例，对程序的正确性是有很大的好处的。
1. JML格式
JML以注释的形式嵌入在代码中，具体的形式有：
// @ annotation /* @ annotation
@ annotation
@ annotation */
2. JML表达式
2.1 原子表达式：
- \result：表示一个非void类型的方法执行所获得的结果，即方法执行后的返回值
- \old(expr)：用来表示一个表达式expr在相应方法执行前的取值
- \not_assigned(x, y, ...)：用来表示括号中的变量是否在方法执行过程中被赋值。
- \not_modified(x, y, ...)：用来表示括号中的变量是否在方法执行过程中取值发生变化
- \nonnullelement(container)：表示容器中存储的对象不会包含有null
- \type(type)：用来表示类型type所对应的对象种类
- \typeof(expr)：用来表示表达式所对应的种类
2.2 量化表达式
- \forall：全称量词修饰的表达式
- \exits：存在量词修饰的表达式
- \sum：给定范围内的表达式的和
2.3 集合表达式
2.4 操作符
- E1<:E2：表示E1是E2的子类型，属于子类型关系操作符
- expr1 <==> expr2, expr1 <=!=> expr2：表示两个布尔表达式是否相同，属于等价关系操作符
- expr1 ==> expr2, expr1 <== expr2：表示两个布尔表达式的推理过程，属于推理操作符
- \nothing, \everything等，这类是对变量的特殊引用，属于变量引用操作符
3. JML方法规格
方法规格的核心内容包括三个方面，前置条件、后置条件和副作用约定。
- 前置条件：requires：表示对输入方法的数据，需要满足的条件
- 后置条件：ensures：表示对于实现方法的策略需要遵循的规则
- 副作用：assignable | modifiable：表示在方法执行的过程中，会被修改的属性数据或者类的静态成员数据。
而对于方法而言，若其不会产生任何的副作用，即不修改任意对象，仅仅是访问的形式，则称其为纯访问方法，在方法名中用 /* pure */表示。
4. JML类型规格
JML类型规格是针对Java程序中的数据类型所设计的限制，常用不变式限制和约束限制。
- 不变式约束：invariant：表示在所有的可见状态下都必须满足的特性，可见状态指：不修改成员变量方法之外的状态。
- 状态变化约束：constraint：对于前序可见状态和当前可见状态的关系约束
5. JML 工具链
JML由于其具有标准的格式，所以同样可以对其进行格式以及语法上的检查，有OpenJML完成对JML的静态检查。
而JML这类语言，其很容易的可以用于构造测试样例，于是也诞生有相关的自动化测试，如JMLUnitNG/IMLunit
二：部署SMT Solver，选择至少三个主要方法来尝试进行验证
三：部署JMLUnitNG/JMLUnit，针对Graph接口实现自动生成测试用例，结合规格对生成的测试用例和数据进行简要的分析
本部分采用的测试样例如下：
package demo;
public class Demo {
/*
@ ensures \result == (num1 + num2);
*/
public static int add(int num1, int num2) {
return num1 + num2;
}
/*
@ ensures \result == (num1 - num2);
*/
public static int sub(int num1, int num2) {
return num1 - num2;
}
/*
@ ensures \result == (num1 / num2);
*/
public static int div(int num1, int num2) {
return num1 / num2;
}
public static void main(String[] args) {
add(4546456, 353546);
sub(1234567, 323598);
div(331235, 0);
}
}
View Code
针对该进行自动生成测试用例，使用下述命令：
java -jar ..\..\openjml\jmlunitng.jar .\demo\Demo.java
生成得到众多测试文件，如
其中较为重要的一些文件解释如下：
- MyGraph_JML_Test.java 为主要的测试类
- MyGraph_InstanceStrategy.java 为生成实例的策略类
- MyGraph_'function':这里为具体的测试方法
对上述进行编译，并且进行运行测试，得到结果如下：
[TestNG] Running:
Command line suite
Failed: racEnabled()
Passed: constructor Demo()
Passed: static add(-2147483648, -2147483648)
Passed: static add(0, -2147483648)
Passed: static add(2147483647, -2147483648)
Passed: static add(-2147483648, 0)
Passed: static add(0, 0)
Passed: static add(2147483647, 0)
Passed: static add(-2147483648, 2147483647)
Passed: static add(0, 2147483647)
Passed: static add(2147483647, 2147483647)
Passed: static div(-2147483648, -2147483648)
Passed: static div(0, -2147483648)
Passed: static div(2147483647, -2147483648)
Failed: static div(-2147483648, 0)
Failed: static div(0, 0)
Failed: static div(2147483647, 0)
Passed: static div(-2147483648, 2147483647)
Passed: static div(0, 2147483647)
Passed: static div(2147483647, 2147483647)
Failed: static main(null)
Failed: static main({})
Passed: static sub(-2147483648, -2147483648)
Passed: static sub(0, -2147483648)
Passed: static sub(2147483647, -2147483648)
Passed: static sub(-2147483648, 0)
Passed: static sub(0, 0)
Passed: static sub(2147483647, 0)
Passed: static sub(-2147483648, 2147483647)
Passed: static sub(0, 2147483647)
Passed: static sub(2147483647, 2147483647)
===============================================
Command line suite
Total tests run: 31, Failures: 6, Skips: 0
===============================================
Process finished with exit code 0
View Code
由于测试的过程中均采用的是int类型，其在测试时，采用大量的边缘数据进行测试，即大量使用0，最大正值以及最小负数等进行测试，以对边缘数据进行监控。
而本次实验中产生了6项错误，其中基本为除零错误，但是可以发现，对于溢出的情况，这里并没有报错，表示这里的溢出根据JML的书写规则是合法的，若需要监控溢出，应该在JML中扩大数据范围，进行测试。
四：按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构
4.1 作业9
作业9只需要根据规格实现相应的内容即可，难度较低，结构如下：
在该实现中，采用双HashMap的结构，对Path和id分别进行索引，如下：
HashMap<MyPath, Id> HashMap<Id, MyPath>
这样在检索过程中的效率较高。
而针对不同点的检索，需要将复杂的搜索均摊到无法优化的指令中去，也就是说在加点的过程中，就可以开始统计不同点的个数，这样要不同点的个数的时候只需要直接取即可。
4.2 作业10
在作业10中，新增的图的管理，对此，我新建了一个类名为Matrix用邻接矩阵来存储改图，并且在该类中进行是否邻接，是否可达，最短距离等计算，采用弗洛伊德算法进行计算最短距离。
最短距离：
在每次加点的过程中，更新matrix图，并且同时计算最短距离。
是否存在边：
这里需要维护一个边的集合，因为两个点之间是否存在边，不可以通过两点之间最短距离来判断，如点2 到 点2存在一个边，但是其最短距离为0，这样无法判断。
是否连通：
这里仅仅需要根据最短距离来判断即可，若两个点之间的最短距离不为INF，则表示两点可达。
4.3 作业11
在作业11中，对于图的分析更进一步了，需要对图建立其有层次的联系，我的框架图如下：
同作业10，我将复杂的计算全部放在了matrix中。而针对不同的路径的计算，同样都采用了弗洛伊德算法进行计算。
首先，对于不同的Path在自己的Path中利用弗洛伊德算法，算出该条路径上两两之间的最短距离，最少消费等等，得到一个较低层次的结果。
再在全局中，利用不同Path上的不同点，再进行更新最短距离，实现一个两级的最短距离的层次算法，这样的时间复杂度为n^3 * 50，是可以接受的，由于每个Path是不变的，仅需要在addPath的阶段计算即可，计算的开销较小。
如何计算不同的指标
针对于不同的指标，实际上都是计算最小值的一个过程，仅在更新两个点之间的距离时产生不同，在更新时根据是否需要换乘等进行计算即可。
五：按照作业分析代码实现的bug和修复情况
5.1 作业9
作业9中，是第一次接触这类作业，对时间开销没有认真的考虑，仅仅在结构上采用了可能会更加省时的结构，但是没有将需求进行拆解分摊，导致了TLE。
针对作业9，也利用Python进行了相应的测试，测试代码如下，对正确性及时间都有所考察
1 import os
2 import time
3 import random
4
5 instructions1 = [
6 "PATH_ADD", # 节点序列
7 "PATH_REMOVE", # 节点序列
8 "PATH_REMOVE_BY_ID", # id
9 "PATH_GET_ID", # 节点序列
10 "PATH_GET_BY_ID", # id
11 "CONTAINS_PATH", # 节点序列
12 "CONTAINS_PATH_ID" # id
13 ]
14 instructions2 = [
15 "PATH_COUNT", # 空
16 "PATH_SIZE", # id
17 "PATH_DISTINCT_NODE_COUNT", # id
18 "DISTINCT_NODE_COUNT", # 空
19 "COMPARE_PATHS", # id id
20 "PATH_CONTAINS_NODE" # id 节点
21 ]
22
23 id = 0
24 node_length = 1000
25 id_list = []
26 nodes_list = []
27 instr1 = 0
28 instr2 = 0
29 instruction_list = []
30 output_list = []
31 input_list = []
32
33
34 def make_instruction():
35 for instr in instruction_list:
36 count, lst = instr[0], instr[1]
37 count1 = count // 10
38 count2 = count % 10
39 string = ""
40 if count1 == 1:
41 string = instructions1[count2 - 1] + " "
42 else:
43 string = instructions2[count2 - 1] + " "
44 for item in lst:
45 string = string + str(item) + " "
46 input_list.append(string)
47
48
49 def print_input():
50 for item in input_list:
51 print(item)
52
53
54 def print_output():
55 for item in output_list:
56 print(item)
57
58
59 def gen_data():
60 """
61 for i in range(20):
62 random1()
63 for j in range(20):
64 random2()
65 """
66 while instr1 + instr2 != 3000:
67 if instr1 == 300:
68 random2()
69 continue
70
71 if instr2 == 2700:
72 random1()
73 continue
74
75 num = random.random()
76 if num < 0.1:
77 random1()
78 else:
79 random2()
80 make_instruction()
81
82
83 def random1():
84 num = random.randint(-4, 7)
85 if num <= 1:
86 judge, result = random1_1()
87 elif num == 2:
88 judge, result = random1_2()
89 elif num == 3:
90 judge, result = random1_3()
91 elif num == 4:
92 judge, result = random1_4()
93 elif num == 5:
94 judge, result = random1_5()
95 elif num == 6:
96 judge, result = random1_6()
97 elif num == 7:
98 judge, result = random1_7()
99 if judge == False:
100 pass
101 else:
102 global instr1
103 instr1 += 1
104 instruction_list.append(result)
105
106
107 def random2():
108 num = random.randint(1, 6)
109 if num == 1:
110 judge, result = random2_1()
111 elif num == 2:
112 judge, result = random2_2()
113 elif num == 3:
114 judge, result = random2_3()
115 elif num == 4:
116 judge, result = random2_4()
117 elif num == 5:
118 judge, result = random2_5()
119 elif num == 6:
120 judge, result = random2_6()
121 if judge == False:
122 pass
123 else:
124 global instr2
125 instr2 += 1
126 instruction_list.append(result)
127
128
129 def random1_1():
130 lst = []
131 for i in range(node_length):
132 num = random.randint(1, node_length)
133 lst.append(num)
134 nodes_list.append(lst)
135 global id
136 id += 1
137 id_list.append(id)
138 output_list.append("Ok, path id is {}.".format(id))
139 return True, [11, lst]
140
141
142 def random1_2():
143 if nodes_list == []:
144 return False, []
145 num = random.randint(1, 2)
146 if num == 1:
147 lst = []
148 for i in range(node_length):
149 lst.append(random.randint(1, node_length))
150 if lst not in nodes_list:
151 output_list.append("Failed, path not exist.")
152 else:
153 index = nodes_list.index(lst)
154 nodes_list.pop(index)
155 num = id_list.pop(index)
156 output_list.append("Ok, path id is {}.".format(num))
157 return True, [12, lst]
158 else:
159 num = random.randint(1, len(nodes_list))
160 lst = nodes_list.pop(num - 1)
161 num = id_list.pop(num - 1)
162 output_list.append("Ok, path id is {}.".format(num))
163 return True, [12, lst]
164
165
166 def random1_3():
167 if id_list == []:
168 return False, []
169 num = random.randint(1, 2)
170 if num == 1:
171 num = random.randint(1, id)
172 if num not in id_list:
173 output_list.append("Failed, path id not exist.")
174 else:
175 index = id_list.index(num)
176 id_list.pop(index)
177 nodes_list.pop(index)
178 output_list.append("Ok, path removed.")
179 return True, [13, [num]]
180 else:
181 num = random.randint(1, len(id_list))
182 nodes_list.pop(num - 1)
183 lst = [id_list.pop(num - 1)]
184 output_list.append("Ok, path removed.")
185 return True, [13, lst]
186
187
188 def random1_4():
189 if nodes_list == []:
190 return False, []
191 num = random.randint(1, 2)
192 if num == 1:
193 lst = []
194 for i in range(node_length):
195 lst.append(random.randint(1, node_length))
196 if lst not in nodes_list:
197 output_list.append("Failed, path not exist.")
198 return True, [14, lst]
199 else:
200 index = nodes_list.index(lst)
201 output_list.append("Ok, path id is {}.".format(id_list[index]))
202 return True, [14, lst]
203 else:
204 num = random.randint(1, len(nodes_list))
205 output_list.append("Ok, path id is {}.".format(id_list[num - 1]))
206 return True, [14, nodes_list[num - 1]]
207
208
209 def random1_5():
210 if id_list == []:
211 return False, []
212 num = random.randint(1, 2)
213 if num == 1:
214 num = random.randint(1, id)
215 if num not in id_list:
216 output_list.append("Failed, path id not exist.")
217 return True, [15, [num]]
218 else:
219 index = id_list.index(num)
220 path = nodes_list[index]
221 string = ""
222 for item in path:
223 string += str(item) + ", "
224 string = string[:-2]
225 output_list.append("Ok, path is (" + string + ").")
226 return True, [15, [num]]
227 else:
228 num = random.randint(1, len(id_list))
229 path = nodes_list[num - 1]
230 string = ""
231 for item in path:
232 string += str(item) + ", "
233 string = string[:-2]
234 output_list.append("Ok, path is (" + string + ").")
235 return True, [15, [id_list[num - 1]]]
236
237
238 def random1_6():
239 num = random.randint(1, 2)
240 if num == 1:
241 if nodes_list == []:
242 return False, []
243 num = random.randint(1, len(nodes_list))
244 output_list.append("Yes.")
245 return True, [16, nodes_list[num - 1]]
246 else:
247 lst = []
248 for i in range(node_length):
249 num = random.randint(1, node_length)
250 lst.append(num)
251 if lst in nodes_list:
252 output_list.append("Yes.")
253 else:
254 output_list.append("No.")
255 return True, [16, lst]
256
257
258 def random1_7():
259 if id == 0:
260 return False, [17, [0]]
261 else:
262 num = random.randint(1, id)
263 if num in id_list:
264 output_list.append("Yes.")
265 else:
266 output_list.append("No.")
267 return True, [17, [num]]
268
269
270 def random2_1():
271 output_list.append("Total count is {}.".format(len(id_list)))
272 return True, [21, []]
273
274
275 def random2_2():
276 if id_list == []:
277 return False, [22, [0]]
278 num = random.randint(1, id)
279 if num not in id_list:
280 output_list.append("Failed, path id not exist.")
281 else:
282 index = id_list.index(num)
283 output_list.append("Ok, path size is {}.".format(len(nodes_list[index])))
284 return True, [22, [num]]
285
286
287 def random2_3():
288 if id == 0:
289 return False, [22, [0]]
290 num = random.randint(1, id)
291 if num not in id_list:
292 output_list.append("Failed, path id not exist.")
293 else:
294 index = id_list.index(num)
295 lst = nodes_list[index]
296 lst = set(lst)
297 output_list.append("Ok, distinct node count of path is {}.".format(len(lst)))
298 return True, [23, [num]]
299
300
301 def random2_4():
302 lst = set([])
303 for item in nodes_list:
304 lst = lst | set(item)
305 output_list.append("Ok, distinct node count is {}.".format(len(lst)))
306 return True, [24, []]
307
308
309 def random2_5():
310 if len(id_list) < 2:
311 return False, [25, [1, 2]]
312 lst = [i + 1 for i in range(id)]
313 lst = random.sample(lst, 2)
314 id1 = lst[0]
315 id2 = lst[1]
316 if id1 in id_list and id2 in id_list:
317 index1 = id_list.index(id1)
318 index2 = id_list.index(id2)
319 judge = compare_lst(nodes_list[index1], nodes_list[index2])
320 if judge == -1:
321 output_list.append("Ok, path {} is less than to {}.".format(id1, id2))
322 elif judge == 1:
323 output_list.append("Ok, path {} is greater than to {}.".format(id1, id2))
324 return True, [25, [id1, id2]]
325 else:
326 output_list.append("Failed, path id not exist.")
327 return True, [25, [id1, id2]]
328
329
330 def random2_6():
331 if len(id_list) == 0:
332 return False, [26, [0, 0]]
333 num1 = random.randint(1, id)
334 num2 = random.randint(1, node_length)
335 if num1 in id_list:
336 index = id_list.index(num1)
337 path = nodes_list[index]
338 if num2 in path:
339 output_list.append("Yes.")
340 else:
341 output_list.append("No.")
342 else:
343 output_list.append("Failed, path id not exist.")
344 return True, [26, [num1, num2]]
345
346
347 def compare_lst(lst1, lst2):
348 len1 = len(lst1)
349 len2 = len(lst2)
350 if len1 < len2:
351 length = len1
352 else:
353 length = len2
354 for i in range(length):
355 if lst1[i] < lst2[i]:
356 return -1
357 elif lst1[i] > lst2[i]:
358 return 1
359 if len1 < len2:
360 return -1
361 elif len1 > len2:
362 return 1
363 else:
364 return 0
365
366
367 def test():
368 # gen_data()
369 # print_input()
370 # print_output()
371 # '''
372 # f = open("input.txt", "w")
373 # for line in input_list:
374 # f.write(line + "\n")
375 # f.close()
376 # f = open("standard.txt", "w")
377 # for line in output_list:
378 # f.write(line + "\n")
379 # f.close
380 # '''
381 begin_time = time.clock()
382 os.system("cat input.txt|java -cp .;D:/My_code/JAVA/OO9/specs-homework-1-1.1-raw-jar-with-dependencies.jar Main>output.txt")
383 end_time = time.clock()
384 print("Time used = ", end_time - begin_time)
385 '''
386 f = open("standard.txt", "r")
387 lines_standard = f.readlines()
388 f.close()
389
390 f = open("output.txt", "r")
391 lines_out = f.readlines()
392 f.close()
393
394 len1 = len(lines_standard)
395 len2 = len(lines_out)
396 if len1 != len2:
397 print("lines number dismatch")
398 return False
399 else:
400 flag = 1
401 for i in range(len1):
402 line1 = lines_standard[i].strip()
403 line2 = lines_out[i].strip()
404 if line1 != line2:
405 print("in the line {}, different!!!".format(i + 1))
406 flag = 0
407 return False
408 if flag == 1:
409 print("Congratulations, you are the same with WL")
410 return True
411 '''
412 return True
413
414
415 if __name__ == "__main__":
416 for i in range(1):
417 judge = test()
418 if not judge:
419 break
420 id = 0
421 node_length = 1000
422 id_list = []
423 nodes_list = []
424 instr1 = 0
425 instr2 = 0
426 instruction_list = []
427 output_list = []
428 input_list = []
View Code
5.2 作业10
作业10在作业9的基础上知道需要进行时间上的分摊，在进行相应的分摊后，便也没有超时。
针对作业10，也利用Python进行相应的大规模的测试，该代码部分由17376482同学实现：
1 from os import system
2 import time
3 import random
4 from queue import Queue
5
6 instructions1 = [
7 "PATH_ADD", # 节点序列
8 "PATH_REMOVE", # 节点序列
9 "PATH_REMOVE_BY_ID", # id
10 ]
11 nodes_graph = {}
12 distance = {}
13 instructions2 = [
14 "PATH_GET_ID",
15 "PATH_GET_BY_ID",
16 "CONTAINS_PATH",
17 "COMPARE_PATHS"
18 ]
19 instructions3 = [
20 "PATH_COUNT", # 空
21 "PATH_SIZE", # id
22 "PATH_DISTINCT_NODE_COUNT", # id
23 "DISTINCT_NODE_COUNT", # 空
24 "CONTAINS_PATH_ID", # id
25 "PATH_CONTAINS_NODE", # id 节点
26 "CONTAINS_NODE", # id 节点
27 "CONTAINS_EDGE", # 节点 节点
28 "IS_NODE_CONNECTED", # 节点 节点
29 "SHORTEST_PATH_LENGTH" # 节点 节点
30 ]
31
32 id = 0
33 node_length = 200
34 id_list = []
35 nodes_list = []
36 instr1 = 0
37 instr2 = 0
38 instr3 = 0
39 instruction_list = []
40 output_list = []
41 input_list = []
42
43
44 def make_instruction():
45 for instr in instruction_list:
46 count, lst = instr[0], instr[1]
47 count1 = count // 10
48 count2 = count % 10
49 if count1 == 1:
50 string = instructions1[count2 - 1] + " "
51 elif count1 == 2:
52 string = instructions2[count2 - 1] + " "
53 else:
54 if count == 0:
55 count += 10
56 string = instructions3[count2 - 1] + " "
57 for item in lst:
58 string = string + str(item) + " "
59 input_list.append(string)
60
61
62 def print_input():
63 for item in input_list:
64 print(item)
65
66
67 def print_output():
68 for item in output_list:
69 print(item)
70
71
72 def gen_data():
73 """
74 while instr1 + instr2 + instr3 != 7000:
75 # instruction type1
76 if instr1 == 20:
77 if instr3 != 6500:
78 random3()
79 continue
80 else:
81 random2()
82 continue
83 # instruction type2
84 if instr2 == 480:
85 if instr1 != 20:
86 random1()
87 continue
88 else:
89 random2()
90 continue
91 if instr3 == 6500:
92 if instr1 != 20:
93 random1()
94 continue
95 else:
96 random2()
97 continue
98 num = random.random()
99 if num < 0.04:
100 random1()
101 elif num < 0.1:
102 random2()
103 else:
104 random3()
105 """
106 for i in range(20):
107 random1()
108 for j in range(24):
109 random2()
110 for k in range(325):
111 random3()
112 make_instruction()
113
114
115 def random1():
116 num = random.randint(-4, 3)
117 # PATH_ADD
118 if num <= 1:
119 judge, result = random1_1()
120 # PATH_REMOVE
121 elif num == 2:
122 judge, result = random1_1()
123 # PATH_REMOVE_BY_ID
124 else:
125 judge, result = random1_1()
126 if judge is False:
127 pass
128 else:
129 global instr1
130 instr1 += 1
131 instruction_list.append(result)
132
133
134 def random2():
135 num = random.randint(1, 4)
136 # PATH_COUNT
137 if num == 1:
138 judge, result = random2_1()
139 # PATH_SIZE
140 elif num == 2:
141 judge, result = random2_2()
142 # PATH_DISTINCT_NODE_COUNT
143 elif num == 3:
144 judge, result = random2_3()
145 # DISTINCT_NODE_COUNT
146 else:
147 judge, result = random2_4()
148 if judge is False:
149 pass
150 else:
151 global instr2
152 instr2 += 1
153 instruction_list.append(result)
154
155
156 def random3():
157 num = random.randint(1, 15)
158 # PATH_COUNT
159 if num == 1:
160 judge, result = random3_10()
161 # PATH_SIZE
162 elif num == 2:
163 judge, result = random3_10()
164 # PATH_DISTINCT_NODE_COUNT
165 elif num == 3:
166 judge, result = random3_10()
167 # DISTINCT_NODE_COUNT
168 elif num == 4:
169 judge, result = random3_10()
170 elif num == 5:
171 judge, result = random3_10()
172 elif num == 6:
173 judge, result = random3_10()
174 elif num == 7:
175 judge, result = random3_10()
176 elif num == 8:
177 judge, result = random3_10()
178 elif num == 9:
179 judge, result = random3_10()
180 else:
181 judge, result = random3_10()
182 if judge is False:
183 pass
184 else:
185 global instr3
186 instr3 += 1
187 instruction_list.append(result)
188
189
190 # PATH_ADD
191 def random1_1():
192 lst = []
193 for i in range(node_length):
194 num = random.randint(0, 260)
195 lst.append(num)
196 if lst in nodes_list:
197 output_list.append("Ok, path id is {}.".format(nodes_list.index(lst)))
198 return True, [11, lst]
199 else:
200 nodes_list.append(lst)
201 global id
202 id += 1
203 id_list.append(id)
204 output_list.append("Ok, path id is {}.".format(id))
205 for i in range(0, len(lst) - 1):
206 add_edge(lst[i], lst[i + 1])
207 add_edge(lst[i + 1], lst[i])
208 bfs()
209 return True, [11, lst]
210
211
212 # PATH_REMOVE
213 def random1_2():
214 if nodes_list == []:
215 return False, []
216 num = random.randint(1, 2)
217 if num == 1:
218 lst = []
219 for i in range(node_length):
220 lst.append(random.randint(1, node_length))
221 if lst not in nodes_list:
222 output_list.append("Failed, path not exist.")
223 else:
224 index = nodes_list.index(lst)
225 nodes_list.pop(index)
226 num = id_list.pop(index)
227 output_list.append("Ok, path id is {}.".format(num))
228 for i in range(0, len(lst) - 1):
229 remove_edge(lst[i], lst[i + 1])
230 remove_edge(lst[i + 1], lst[i])
231 bfs()
232 return True, [12, lst]
233 else:
234 num = random.randint(1, len(nodes_list))
235 lst = nodes_list.pop(num - 1)
236 num = id_list.pop(num - 1)
237 output_list.append("Ok, path id is {}.".format(num))
238 for i in range(0, len(lst) - 1):
239 remove_edge(lst[i], lst[i + 1])
240 remove_edge(lst[i + 1], lst[i])
241 bfs()
242 return True, [12, lst]
243
244
245 # PATH_REMOVE_BY_ID
246 def random1_3():
247 if id_list == []:
248 return False, []
249 num = random.randint(1, 2)
250 if num == 1:
251 num = random.randint(1, id)
252 if num not in id_list:
253 output_list.append("Failed, path id not exist.")
254 else:
255 index = id_list.index(num)
256 id_list.pop(index)
257 lst = nodes_list.pop(index)
258 for i in range(0, len(lst) - 1):
259 remove_edge(lst[i], lst[i + 1])
260 remove_edge(lst[i + 1], lst[i])
261 output_list.append("Ok, path removed.")
262 bfs()
263 return True, [13, [num]]
264 else:
265 num = random.randint(1, len(id_list))
266 del_lst = nodes_list.pop(num - 1)
267 for i in range(0, len(del_lst) - 1):
268 remove_edge(del_lst[i], del_lst[i + 1])
269 remove_edge(del_lst[i + 1], del_lst[i])
270 lst = [id_list.pop(num - 1)]
271 output_list.append("Ok, path removed.")
272 bfs()
273 return True, [13, lst]
274
275
276 # PATH_GET_ID
277 def random2_1():
278 if nodes_list == []:
279 return False, []
280 num = random.randint(1, 2)
281 if num == 1:
282 lst = []
283 for i in range(node_length):
284 lst.append(random.randint(1, node_length))
285 if lst not in nodes_list:
286 output_list.append("Failed, path not exist.")
287 return True, [21, lst]
288 else:
289 index = nodes_list.index(lst)
290 output_list.append("Ok, path id is {}.".format(id_list[index]))
291 return True, [21, lst]
292 else:
293 num = random.randint(1, len(nodes_list))
294 output_list.append("Ok, path id is {}.".format(id_list[num - 1]))
295 return True, [21, nodes_list[num - 1]]
296
297
298 # PATH_GET_BY_ID
299 def random2_2():
300 if id_list == []:
301 return False, []
302 num = random.randint(1, 2)
303 if num == 1:
304 num = random.randint(1, id)
305 if num not in id_list:
306 output_list.append("Failed, path id not exist.")
307 return True, [22, [num]]
308 else:
309 index = id_list.index(num)
310 path = nodes_list[index]
311 string = ""
312 for item in path:
313 string += str(item) + ", "
314 string = string[:-2]
315 output_list.append("Ok, path is (" + string + ").")
316 return True, [22, [num]]
317 else:
318 num = random.randint(1, len(id_list))
319 path = nodes_list[num - 1]
320 string = ""
321 for item in path:
322 string += str(item) + ", "
323 string = string[:-2]
324 output_list.append("Ok, path is (" + string + ").")
325 return True, [22, [id_list[num - 1]]]
326
327
328 # CONTAINS_PATH
329 def random2_3():
330 num = random.randint(1, 2)
331 if num == 1:
332 if nodes_list == []:
333 return False, []
334 num = random.randint(1, len(nodes_list))
335 output_list.append("Yes.")
336 return True, [23, nodes_list[num - 1]]
337 else:
338 lst = []
339 for i in range(node_length):
340 num = random.randint(1, node_length)
341 lst.append(num)
342 if lst in nodes_list:
343 output_list.append("Yes.")
344 else:
345 output_list.append("No.")
346 return True, [23, lst]
347
348
349 # COMPARE_PATHS
350 def random2_4():
351 if len(id_list) < 2:
352 return False, [24, [1, 2]]
353 lst = [i + 1 for i in range(id)]
354 lst = random.sample(lst, 2)
355 id1 = lst[0]
356 id2 = lst[1]
357 if id1 in id_list and id2 in id_list:
358 index1 = id_list.index(id1)
359 index2 = id_list.index(id2)
360 judge = compare_lst(nodes_list[index1], nodes_list[index2])
361 if judge == -1:
362 output_list.append("Ok, path {} is less than {}.".format(id1, id2))
363 elif judge == 1:
364 output_list.append("Ok, path {} is greater than {}.".format(id1, id2))
365 return True, [24, [id1, id2]]
366 else:
367 output_list.append("Failed, path id not exist.")
368 return True, [24, [id1, id2]]
369
370
371 # PATH_COUNT
372 def random3_1():
373 output_list.append("Total count is {}.".format(len(id_list)))
374 return True, [31, []]
375
376
377 # PATH_SIZE
378 def random3_2():
379 if id_list == []:
380 return False, [32, [0]]
381 num = random.randint(1, id)
382 if num not in id_list:
383 output_list.append("Failed, path id not exist.")
384 else:
385 index = id_list.index(num)
386 output_list.append("Ok, path size is {}.".format(len(nodes_list[index])))
387 return True, [32, [num]]
388
389
390 # PATH_DISTINCT_NODE_COUNT
391 def random3_3():
392 if id == 0:
393 return False, [33, [0]]
394 num = random.randint(1, id)
395 if num not in id_list:
396 output_list.append("Failed, path id not exist.")
397 else:
398 index = id_list.index(num)
399 lst = nodes_list[index]
400 lst = set(lst)
401 output_list.append("Ok, distinct node count of path is {}.".format(len(lst)))
402 return True, [33, [num]]
403
404
405 # DISTINCT_NODE_COUNT
406 def random3_4():
407 lst = set([])
408 for item in nodes_list:
409 lst = lst | set(item)
410 output_list.append("Ok, distinct node count is {}.".format(len(lst)))
411 return True, [34, []]
412
413
414 # CONTAINS_PATH_ID
415 def random3_5():
416 if id == 0:
417 return False, [35, [0]]
418 else:
419 num = random.randint(1, id)
420 if num in id_list:
421 output_list.append("Yes.")
422 else:
423 output_list.append("No.")
424 return True, [35, [num]]
425
426
427 # PATH_CONTAINS_NODE
428 def random3_6():
429 if len(id_list) == 0:
430 return False, [36, [0, 0]]
431 num1 = random.randint(1, id)
432 num2 = random.randint(1, node_length)
433 if num1 in id_list:
434 index = id_list.index(num1)
435 path = nodes_list[index]
436 if num2 in path:
437 output_list.append("Yes.")
438 else:
439 output_list.append("No.")
440 else:
441 output_list.append("Failed, path id not exist.")
442 return True, [36, [num1, num2]]
443
444
445 # CONTAINS_NODE
446 def random3_7():
447 if len(id_list) == 0:
448 return False, [37, [0, 0]]
449 num = random.randint(1, 450)
450 flag = 0
451 for i in range(len(nodes_list)):
452 lst = nodes_list[i]
453 if num in lst:
454 flag = 1
455 output_list.append("Yes.")
456 break
457 if flag == 0:
458 output_list.append("No.")
459 return True, [37, [num]]
460
461
462 # CONTAINS_EDGE
463 def random3_8():
464 if len(id_list) == 0:
465 return False, [38, [0, 0]]
466 num1 = random.randint(1, 260)
467 num2 = random.randint(1, 260)
468 if num1 not in nodes_graph:
469 output_list.append("No.")
470 else:
471 lst = nodes_graph.get(num1)
472 if num2 in lst:
473 output_list.append("Yes.")
474 else:
475 output_list.append("No.")
476 return True, [38, [num1, num2]]
477
478
479 # IS_NODE_CONNECTED
480 def random3_9():
481 if len(id_list) == 0:
482 return False, [39, [0, 0]]
483 num1 = random.randint(1, 270)
484 num2 = random.randint(1, 270)
485 if judge_node_in(num1) is False:
486 output_list.append("Failed, node id not exist.")
487 elif judge_node_in(num2) is False:
488 output_list.append("Failed, node id not exist.")
489 elif num1 == num2:
490 output_list.append("Yes.")
491 elif (num1, num2) in distance:
492 output_list.append("Yes.")
493 else:
494 output_list.append("No.")
495 return True, [39, [num1, num2]]
496
497
498 # SHORTEST_PATH_LENGTH
499 def random3_10():
500 if len(id_list) == 0:
501 return False, [30, [0, 0]]
502 num1 = random.randint(1, 265)
503 num2 = random.randint(1, 265)
504 if judge_node_in(num1) is False:
505 output_list.append("Failed, node id not exist.")
506 elif judge_node_in(num2) is False:
507 output_list.append("Failed, node id not exist.")
508 elif num1 == num2:
509 output_list.append("Ok, length is {}.".format(0))
510 elif distance.get((num1, num2)) is not None:
511 output_list.append("Ok, length is {}.".format(distance.get((num1, num2))))
512 else:
513 output_list.append("Failed, node not connected with each other.")
514 return True, [30, [num1, num2]]
515
516
517 def compare_lst(lst1, lst2):
518 len1 = len(lst1)
519 len2 = len(lst2)
520 if len1 < len2:
521 length = len1
522 else:
523 length = len2
524 for i in range(length):
525 if lst1[i] < lst2[i]:
526 return -1
527 elif lst1[i] > lst2[i]:
528 return 1
529 if len1 < len2:
530 return -1
531 elif len1 > len2:
532 return 1
533 else:
534 return 0
535
536
537 def judge_node_in(node):
538 for i in range(len(nodes_list)):
539 lst = nodes_list[i]
540 if node in lst:
541 return True
542 return False
543
544
545 def add_edge(fromNode, toNode):
546 if fromNode in nodes_graph:
547 mid_dict = nodes_graph.get(fromNode)
548 if toNode in mid_dict:
549 mid_dict[toNode] = mid_dict.get(toNode) + 1
550 else:
551 mid_dict[toNode] = 1
552 nodes_graph[fromNode] = mid_dict
553 else:
554 mid_dict = {}
555 mid_dict[toNode] = 1
556 nodes_graph[fromNode] = mid_dict
557
558
559 def remove_edge(fromNode, toNode):
560 mid_dict = nodes_graph.get(fromNode)
561 if mid_dict.get(toNode) == 1:
562 del mid_dict[toNode]
563 else:
564 mid_dict[toNode] = mid_dict.get(toNode) - 1
565 if mid_dict:
566 nodes_graph[fromNode] = mid_dict
567 else:
568 del nodes_graph[fromNode]
569
570
571 def bfs():
572 global distance
573 distance = {}
574 for key in nodes_graph.keys():
575 depth = 1
576 nowqueue = Queue()
577 nextqueue = Queue()
578 nowqueue.put(key)
579 while not nowqueue.empty():
580 nextNode = nowqueue.get()
581 keyMap = nodes_graph[nextNode]
582 for Anode in keyMap.keys():
583 if Anode != key:
584 if not (key, Anode) in distance:
585 distance[(key, Anode)] = depth
586 nextqueue.put(Anode)
587 if nowqueue.empty():
588 depth += 1
589 nowqueue = nextqueue
590 midqueue = Queue()
591 nextqueue = midqueue
592
593
594 if __name__ == "__main__":
595 while True:
596 nodes_graph = {}
597 distance = {}
598 id = 0
599 node_length = 200
600 id_list = []
601 nodes_list = []
602 instr1 = 0
603 instr2 = 0
604 instr3 = 0
605 instruction_list = []
606 output_list = []
607 input_list = []
608 gen_data()
609 f = open("input.txt", "w")
610 for line in input_list:
611 f.write(line + "\n")
612 f.close()
613 f = open("standard.txt", "w")
614 for line in output_list:
615 f.write(line + "\n")
616 f.close()
617 begin_time = time.perf_counter()
618 system("java -cp .;D:/My_code/JAVA/OO10/specs-homework-2-1.2-raw-jar-with-dependencies.jar Main < input.txt > output.txt")
619 end_time = time.perf_counter()
620 print("Time used = {}".format(end_time - begin_time))
621 f = open("standard.txt", "r")
622 lines_standard = f.readlines()
623 f.close()
624 f = open("output.txt", "r")
625 lines_out = f.readlines()
626 f.close()
627 len1 = len(lines_standard)
628 len2 = len(lines_out)
629 if len1 != len2:
630 print("lines number dismatch")
631 break
632 else:
633 flag = 1
634 for i in range(len1):
635 line1 = lines_standard[i].strip()
636 line2 = lines_out[i].strip()
637 if line1 != line2:
638 print("in the line {}, different!!!".format(i + 1))
639 flag = 0
640 break
641 if flag == 1:
642 print("Congratulations, you are the same with the standard!")
643 else:
644 break
View Code
5.3 作业11
作业11出现大面积翻车，在该作业期间，周二看时间节点还是周日，到周四早上惊然发现时间节点是周四晚上，于是从看题开始一个下午速成，在中测结果通过后，时间已不够，没有构造较多测试，导致翻车。
对于该作业完成的期间，思考的过程如下：
拆点作法：
这道题相同id的点，在不同的Path上是不同的，可以将这些点进行拆分形成多个点，并进行链接，从而将该问题转换成一个很简单的点点之间的最短路径问题，但是这样的复杂度激增。
不拆点：
不拆点，仍然需要对相同的id的点进行不同的考虑。
bug出现原因：层次化的方法需要思考细致，在对每条Path完成各自最短路径的计算后，再在全局进行更新时，需要对全局的图首先由所有的Path进行初始化，在缺少这一步的情况下就可能出现问题。
六：阐述对规格撰写和理解上的心得体会
JML规格更像是一种形式验证，从这样的形式验证的角度来保证代码的正确性，既保证了程序的正确性，又不限制算法的实现过程，在理解JML的前提下，代码实现就变得更加简单，感觉在团队合作过程中，相互交流不同函数的要求，不如直接看这类的JML的要求，对程序员而言更直接更能接受。
这几次的作业中大家最终在完成规格的情况下，结果也不尽相同，表示规格的正确性固然重要，但是程序的性能不能由规格定义（虽然可以通过限制时间），仍然需要对架构和方法有清楚的认识。