一、JML语言基础

JML语言是一种java的规格描述语言。它可以无二义性地描述一个类或者方法的行为，并且对类的行为进行规约。从而在具体实现一个类或方法之前，首先了解到其预期功能和行为，提高工程实现的效率。通过JML及其支持工具，不仅可以基于规格自动构造测试用例，并整合了SMTSolver等工具以静态的方式来检查代码实现对规格的满足。

JML语言基础如下：

1.注释结构

JML以javadoc注释的方式来表示规格，每行以@起头。其中行注释为“//@annotation”，块注释为“/*@ annotation... @*/”。

2.表达式

\old(expr)：表示表达式expr在该方法执行前的取值。

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

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

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

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

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

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

3.操作符

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

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

二、JML工具链

openJML可以对JML语言进行语法检查；

JMLUnitNG可以针对JML注释生成测试。

三、架构设计

第一次作业：

第一次作业考虑的较为简单，因此只是简单的把数据存在Map里，也只存了单向的数据，反向查找的时候是用的迭代器进行遍历，因此时间性能很差。

第二次作业：

第二次作业吸取了第一次的教训，加入了Map的双向索引，同时增加了新的EdgeMap类实现了邻接表的功能，大体结构与第一次相比并没有太大的变化。。

第三次作业：

第三次作业在第二次作业的基础上增加了对几种不同边权的最短路径的求解，因此增加了FloydCalculator类计算最短路径，同时将无向图的BFS染色提出设置为ColoredGraph类。FloydCalculator类通过类似函数指针的语法实现对不同边权的适应。

四、bug及其修复

第一次作业没有很好的计算算法时间复杂度的需求，使用了Map的Iterator来检索元素，因此超时了很多点。在第二次作业中吸取了教训增加了双向的Map及其检索，没有出现bug。在第三次作业中，对前两次作业进行了比较大幅度的重构，同时求最短路径的时候结果的储存没有做好，因此出现了很多问题。

五、个人总结

这三次作业让我切身的明白了规格化设计在大规模软件编程过程中的重要意义。以前我一直没有认识到软件工程的重要意义，认为只要算法正确，程序实现都只是小问题，但是这三次作业使我明白了，正确的算法也是要建立在正确的实现方式的基础上的，而正确的实现则是要通过规格化设计来进行形式上的保证的。在接下来的程序设计中，特别是团队协作的编程过程中，我会更加注意规格化软件设计以及相关编程工具的应用。