测试与正确性论证的效果差异及其优缺点
测试是利用测试代码，通过编写测试用例来验证代码是否能正常完成所要求的功能，自动测试相较于正确性论证来说更加的直观，直接测试代码的功能，而正确性论证是在JSF的基础上用表达式和语言梳理代码的结构并论证其功能的正确实现。
测试的优点是直观明确，缺点是通过样例测试正确性，样例的编写若是有疏失不完善，那么，测试就有疏漏。
正确性论证虽然通过自然语言论证，比较复杂冗长，但是对代码实现的逻辑做一个完整的梳理比较不容易有疏漏，但缺点，也就是复杂带来的效率下降也是一定的。
OCL
OCL是对象约束语言（Object Constriant Language）的简称，它是一种指示用户建模系统中的限制方式。它是UML可选的附加内容，可以用来更好地定义对象的行为，并为任何类元指定约束。它和JSF同样都是声明式的语言，都有前置条件、后置条件和不变式，但它不像JSF一样完全用逻辑表达式，它是有许多基本的数据类型的，且每个表达式都是有类型的。
第十四次作业
1.类图
2.顺序图
3.状态图
总结
1.知识点
第一个单元主要是一些简单的任务让我们熟悉面向对象的思想和java的使用。
有了第一个单元作为基础，第二单元便开始加大难度，学习了多线程和线程安全相关的内容。
接着第三个单元便是规格化设计，训练我们在大型工程项目的规范化开发以及合作与沟通的技巧。
第四个部分是测试，包括单元化测试以及正确性论证。
2.我在前期刚起步的时候代码都很不完善，一直挣扎到了中后期才有所好转，在最后一次作业时我重构了大部分原来的代码，整体程序结构精简很多，总的来说还是有所进步的。
3.工程化开发有参与合作人员多、代码规模大、程序健壮性要求高等特点，其中有很多难点需要用规范化的方法来解决，平时个人单机编程，可能很难体会到这些规范和方法的重要性，但实际上这些条条框框保证了开发的效率和后续维护的方便性。
4.在后期的作业中训练重点是在测试和规范，但由于前几次作业留下来的习惯，很多同学仍然会很在意指导书新增的功能，而由于训练重点不在此，指导书中对新增功能的要求往往不够规范和详细，希望可以从中找到一个平衡点。