一、JML语言理论基础及其工具链

1. JML语言理论基础

JML是用于对Java程序进行规格化设计的一种表示语言，是一种行为接口规格语言(Behavior Interface Specification Language，BISL),基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。一般而言，JML有两种主要的用法：

1) 开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。

2) 针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。

2. JML工具链

二、部署SMT Solver验证

三、部署JMLUnitNG,自动生成测试样例

四、三次作业架构设计与迭代

五、Bug分析与修复

六、心得体会

1. 规格撰写与理解

通过这一单元三次作业还有课上的两次实验写下来，对规格也算是有了更深的理解。规格是对开发人员的规范，为严格的程序设计提供了一套行之有效的方法。我们第三单元通过三节课的学习，了解了类规格，方法规格，数据规格的写法，最重要的是为什么要写规格。总结来说，类规格定义了与用户的契约，也定义了开发人员必须遵从的规约。方法规格则由前置条件，后置条件和副作用组成，这是一个方法对实现者的规约。而数据规格则是类有效性的控制条件，constraint和invariant分别定义了数据状态需要满足的条件和数据修改需要满足的条件。

规格化设计是一种致力于保证程序正确性的设计方法，它本质上是一种设计方法。我们可以利用WARRANTY方法来看待规格化设计。

Step1(Why): 为什么需要这个方法？
Step2(Acceptance criteria): 这个方法所提供结果正确的判定条件是什么？
Step3(cleaR Requirement): 这个方法是否需要对调用者做出一些要求，从而确保能够产生正确结果？
Step4(ANticipated changes): 这个方法执行期间是否需要修改输入数据或者所在对象数据？
Step5(TrustY): 无需代码即可确认其语义

契约式设计是一种基于信任机制+权利义务均衡机制的设计方法学，JML的诞生正是源自于契约式设计的需要。通过本单元的学习，我感受到了通过规格设计，可以更容易获得简洁和职责单一的设计和实现（复杂方法会导致直接写不清楚相应的规格）。另一方面，经过实验和作业训练会发现，在很多情况下设计和撰写规格要比编写代码难。一旦规格确定了，其实实现代码就变成了一个相对简单的事情，除非涉及复杂的算法要求。因此，多理解规格使用规格化设计，对我们今后的软件开发大有裨益。

2. 想说的话

随着第三单元的结果，12周OO生涯已经过去了。本学期的OO课程也接近尾声，本学期OO课程做了非常大的改革，目前看来都是非常成功的，再次感谢老师助教们的付出。最后一单元是UML相关，希望自己继续加油，给本学期的OO课程画上一个圆满的句号。

2019年北航OO第三次博客总结

原文：https://www.cnblogs.com/ljyhero/p/buaaoo-ljy3.html