标签：基础应用 上进 统一 接口 algo class 而不是 const 耦合度
JML 理论基础：
JML建立契约式编程的基础上，是一种实现契约式编程的规格化语言。顾名思义，契约式编程，是供求双方建立在一定的契约上进行软件的开发和应用。类似于在共同完成这一个工程的时候我们对于每个方法都以一个供求双方都统一并且详细知晓的合同，在这个合同上，供应方要不多不少完成合同上的所有要求，需求方的可提出的需求范围只限于合同上的明确条文。这样同时明确了双方的权利和义务。而产生契约式编程的背景是很多工程的开发过程权责混乱，导致管理混乱开发低效。而契约式编程正是切中了这一痛点，明确权责，提高管理，提升效率。
JML是其中的一种实现语言。通过规定一种方法的先验条件，作用域，和后置条件等等来规范一个方法。达到契约式编程的目的。
JML常用语法梳理：（以下均为JML Level 0）
a. 注释结构：
b. JML表达式：
\result:非void类型方法执行获得的结果；\old(expr):表达式expr在响应方法执行前的取值；\forall表达式:全称量词修饰的表达式，表示对于给定范围内的元素 ，每个元素都应该满足相应的约束；\exists表达式：存在两次修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束；\sum表达式：返回给定范围内的表达式的和；num_of表达式：返回指定变量中满足相应条件的取值个数；<==>:等价关系操作符;==>:逻辑推理操作符;\nothing \everything:变量引用操作符;c. 方法规格：
requires P;ensures P;assignable P;signals (***Exception e) b_expr;d. 类型规格：
invariant;constraint;JML相关工具
Open JML
根据方法的实现对方法进行语法检查、程序的静态检查、程序的运行时检查；
JML UnitNG
根据JML自动生成测试样例测试程序。
// TestJMLUnit/Test.java
package TestJMLUnit;
public class Test {
/*@ public normal_behaviour
@ ensures \result == lhs - rhs;
*/
public static int compare(int lhs, int rhs) {
return lhs - rhs;
}
public static void main(String[] args) {
compare(114514,1919810);
}
}首先运行jmlunitng.jar包生成相关java文件
java -cp jmlunitng.jar TestJMLUnit/Test.java
之后编译所有生成的java文件
javac -cp jmlunitng.jar TestJMLUnit/*.java
运行openjml.jar进行运行时检查：
java -cp openjml.jar -rac TestJMLUnit/Test.java
最后使用TestNG进行测试;
java -cp jmlunitng.jar TestJMLUnit.Test_JML_Test
运行结果如下：
第一次作业的结构比较简单，所以只有两个类：path的实现类和容器的实现类。
?实现path采用ArrayList和HashMap的多数据维护数据，分别对应查询不重复节点数和查找 对应下标位置的节点；实现容器的时候采用的是多个HashMap分别对应着查询id，path，和不重复节点数。
类图如下：
本次作业没有产生bug。
第二次作业中由于加入了图操作，考虑到下一步作业的扩展性，应该是进一步扩展图的操作，因此对程序的结构进行了一定的重构：
在重构之后，外层的PathContainer结构实现的类更佳类似于一个shell，而具体的运行的都移动到了Graph的Manager，并且把图的各个元素尽量各自通过一个容器管理。但是由于当出现图构指令的时候，不仅需要更新图的邻接矩阵，也需要对各个元素的容器更新。由此会体现出各个容器还欠缺一些独立性。再者本次作业中的图的管理和相关的计算还没有做出分离。
本此作业中只是要求求出两个节点之间最短距离。我采用的是floyd算法，每次更新算法的时候通过一个标识符标识当前图的结构已经更新从而需要重新调用floyd，否则直接获取邻接矩阵中的数值即可。本次作业中把节点的连通性和节点之间的距离计算放到一块，通过查看距离是否大于INFO值判断两个节点是否连通。
对于临界矩阵的实现方法，我采用的是两层的HashMap，第一层key是出发节点，第二层的key是到达节点。存储的数据是当前计算出的两个节点之间的最短距离。
重构之后的类图如下：
依赖度如下图：
本次作业中进行了一定的重构，达到了一定的效果，扩展性增大。但是结构仍然有一定的扩展空间：扩大各个元素容器管理类的独立性实现真正的各个元素只是有相应类管理；分离图的结构管理和图的相关算法的分离。
本次作业没有产生bug，但是对比其他同学的程序来看。我的作业运行时间其实是有些危险，也代表着算法方面有优化空间。本次采用的floyd算法是默认每次都是算出每两个节点之间的距离，由此会产生很多冗余的数据。由此带来的运行时间浪费。
第三次作业进一步增加图的功能模拟地铁站的运行，由此带来的重构：
Edge对象，使得边的管理不在是总是通过两个节点来查找；PathManager，使得path的管理从图中剥离出来；GraphAlgorithm和图的结构管理和更新的类GraphMatain，通过图的Manager调度两者的协同合作。重构之后，图的管理类中只需要管理各个元素的管理类，进一步降低耦合度。并且抽象出图算法类，使得图的算法设计的维护和debug难度都有所下降。
本次作业算法实现有两个版本：初级版本是采用的记录每个边个点的路径id在调用图算法计算的时候侦测到id变化就会在权值上增加换乘的代价。在实现之后发现由于两条path不仅可以包含相同的节点，也可以包含相同的边，并且数量还没有限制，由此带来的是一条边可以有多个身份，换乘不好确定。(一口老血，算法还是太渣)第二版本是用了wjy同学算法，同一路径先连边，不同path连边增加换乘代价。对于不同的需求，增加相应的换乘权重。对于连通块的计算，我使用的方法是把连通性和连通块合并，采用染色的方法计算连通块的数量。
通过依赖度的分析也可以看出来，图的管理类直接控制各个元素的管理，而各个元素的管理类互相不干涉。以下数据也可以看出本次重构基本上达到了初始的降低耦合度，降低各个类的依赖度的目的。比第二次作业程序结构有进一步的提升。基本上填补了第二次作业重构未涉及的地方。
其实在第二次作业中已经感受到，一个好的程序结构会带来的巨大遍历和工程编写的难度的下降。第三次作业更加明显：如果第二次作业能够预先的分离出来图算法的类，进行单独的封装只是通过图的管理接收图的数据，那么第三次作业就可以只是修改图的算法，增加一些对外的接口就可以完成第三次作业的要求。这也是我对于好的程序结构带来巨大好处感受最深的一次。（这大概也是我写的最面向对象的一次作业）
虽然本次作业写出了自己最面向对象的作业，但是作业的正确性第一位大概让我吃了。虽然没有出现最担心的TLE，但是出现WA声一片。在第三次作业中由于想无重复的访问一个path的所有节点，所以就把path的iterator修改成了HashMap的iterator，就是这一改，使得在获取路径的时候输出的节点是乱序而不是按照原来的顺序输出，就这样强测完美躲过正确答案。改回迭代器之后,成功debug。(迭代器引发的惨案)
只能说是自己的测试不充分，把测试都放在了程序新添加的功能上了没有去保证原本功能的正确性。
? 首先是对于这三次作业的体验其实并不是很好，其实重构程序的结构并没有占用很长的时间，而大部分时间（后两次作业）都在于怎么设计和优化算法。其实由于作业的结构没有多么的复杂，其实不需要一个很完美的结构，但是必须需要一个完美的算法。并且对于open JML的使用体验不好，课程组的给的规格Open JML有些不支持，因此其实在这个学习过程中无论是测试还是编写程序过程中都没怎么使用Open JML。更多的测试方法还是大量数据集的黑盒测试以及使用Junit测试。
? 但是从作业中也感受到，规格化编程的思想是一个很好的东西。契约性的编程更加清晰的划分了各个方法的操作边界在哪里。对于方法执行功能有一个很有逻辑性和确定性的描述很好的避免了自然语言的二义性，对于工程的开发是一个很好的开发方式。通过这种开发方式，可以很好的做到分工明确。各个部分的协调沟通效率会大大提高。但是从第三次作业也感受到，为了一个方法的规格描述，有时候却要增加一些没必要实现的方法的规格描述。并且当方法复杂的时候，规格描述会变得极其冗长，读起来困难并且要串联着其他方法的规格一起理解，反而增大了时间上的浪费。其实在OS的实验中，其中一些方法的注释也是一种契约编程，而方法的规格简洁易懂，可能因为方法不太复杂，但是说明精巧的自然语言描述也不失为一种好的规格描述方法。
标签：基础应用 上进 统一 接口 algo class 而不是 const 耦合度
原文地址：https://www.cnblogs.com/lijin1905/p/10899466.html
