标签：sign 重要 相关 复杂度 没有 梳理 迭代 详细 floyd
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言
（Behavior Interface Specification Language，BISL），基于Larch方法构建。通过JML及其支持工具，不仅可以基于规格自动构造测试用例，并整合了SMT Solver等工具以静态方式来检查代码实现对规格的满足情况。一般而言，JML有两种主要的用法：
（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规
格。
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。
方法规格是JML的重要内容，本手册仅涉及最基础的部分，而不引述JML扩展部分的内容。方法规格的核心内容包括三个方面，前置条件、后置条件和副作用约定。
1.前置条件(pre-condition)
前置条件通过requires子句来表示： requires P; 。其中requires是JML关键词，表达的意思是“要求调用者确保P为
真”。注意，方法规格中可以有多个requires子句，是并列关系，即调用者必须同时满足所有的并列子句要求。
2.后置条件(post-condition)
后置条件通过ensures子句来表示： ensures P; 。其中ensures是JML关键词，表达的意思是“方法实现者确保方法执行返回结果一定满足谓词P的要求，即确保P为真”。
3.副作用范围限定(side-effects)
副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响。从方法规格的角度，必须要明确给出副作用范围。JML提供了副作用约束子句，使用关键词 assignable或modifiable。
无
首先根据讨论区中的方法配置OpenJML，进行简单的check进行测试。
随后根据讨论区中的代码进行微调，进行一个sub减法的测试。代码如下
package demo;
public class Demo {
/*@ public normal_behaviour
@ ensures \result == lhs - rhs;
*/
public static int sub(int lhs, int rhs) {
return lhs - rhs;
}
public static void main(String[] args) {
sub(114514,1919810);
}
}测试时，依据讨论区中的方法配置好文件，随后的指令和结果如下。
可见，自动测试针对一些极端情况进行了测试，实际使用时可将命令写在脚本中，从而缩短测试时的工作量。
本次作业仅要求实现PathContainer，其中需要特别处理的方法为getDistinctNodeCount，若是每次都遍历所有Path，势必会因时间产生问题。总体思路为建立三张HashMap，两张保存Path，分别以path和pathid为键，对应的pathid或path为值，另准备一张图保存所有节点的个数，在添加或移除path时更新节点图，并移除数量为0的Node，查询时返回该Map的size即可。其余方法根据规格直接填写即可。
本次作业要求将Path整合成Graph并实现Graph的相关操作，若是以常规方法仍需大量遍历所有Path，构造时主要需要设计的是采用怎样的数据结构保存信息，将复杂度分散到add和remove中。我的设计为，在作业九的基础上，新增HashMap<String,int>用于保存边的数量，原理同distinctnode。同时准备一个静态数组，每次add和remove时更新，用于保存所有点之间的最短路径，采用floyd算法实现，isConnect方法只需要查看数组中是否存在最短路径即可。
第十一次作业仍继承了前一次的框架，只是对保存边的hashmap由<String,Integer>改为<Integer,ArrayList< Integer>>，新增三个静态数组用于保存ticket，unpleasant，trans信息，新增一个int成员保存连通块数量。静态数组更新全部在add和remove阶段完成，采用算法为王嘉仪同学在讨论区分享的floyd改良算法。对方法没有进行大规模修改，仅实现新的接口，调整add和remove时的功能，以及更改了containsEdge方法（因为更改了hashmap，但笔者没有对此方法进行回归测试，导致强测时此步出问题，望大家引以为戒，修改之前的方法一定进行回归测试）。
从整体来看，虽然在第九次和第十一次因为低级错误损失了不少分数，但是通过半学期的oo训练，我的架构已经取得了很大的进步，在整体迭代开发过程中代码都得到了复用，前一次作业中的信息在新的作业里可直接使用（例如distinctnode这张hashmap在第十次和第十一次作业都得到了复用）。
第九次作业中的bug为我错误的理解了字典序以及刚开始我采用的是两张hashmap而不是三张，主要是由于时间规划的不合理导致匆匆完成代码，没有进行充分地设计和理解，bug修复阶段很顺利，修改compare方法以及增加hashmap后完成。
第十一次作业的bug为containsEdge方法没有进行回归测试，导致某些边的查阅会导致空指针异常，修改后即可。
经过本单元的学习，我对jml规格编写和实现上有很大的收货。我认为这是一个在团队开发中异常重要的环节，若是个人开发或是小团队开发，编写规格很难起到良好的成效，反而可能拖慢节奏。但在大规模开发中，若是没有规格对程序员进行约束，成员间的协作将出现混乱，代码之间无法相互配合。规格的存在就是保证代码的功能一定符合要求，无论是以怎样的方法及风格实现，都具有相同的功能。程序员在实现规格时可清晰的理解到自己所要完成的任务，编写规格的训练也可以帮助我们更好的理解规格实现，以及对代码功能进行更详细的分析。
标签：sign 重要 相关 复杂度 没有 梳理 迭代 详细 floyd
原文地址：https://www.cnblogs.com/xuejingxuan/p/10906859.html
