测试与正确性论证
首先我们先来说一下这两个概念的差异所在。所谓测试，是指：基于前置条件和后置条件对输入划分并抽样产生测试数据，检查方法执行输出是否满足后置条件。而正确性论证，是指：针对格式化的规格和代码实现，人工方式对代码逻辑进行分析，确认是否所有满足前置条件的输入都能产生满足后置条件的结果。
然后我们来谈一下两者的优缺点。测试的优点在于易于实施，这也是其在工程中被广泛使用的原因；而它的缺点在于无法保证正确性，毕竟只是对于输入的抽样测试，可能无法真正地从代码层面来找出程序设计的错误。对于正确性论证，它的优点在于是形式化验证和测试的折衷，其结合了形式验证与自然语言层次逻辑，淡化了形式验证的高成本的同时，也一定程度提高了验证的正确性；而它的缺点在于无法确保自然语言层次逻辑推理的严谨性，这也是其淡化形式化验证的结果。
对于这两者的理解，可以在一定程度上帮助我前几次作业的完成，也可能帮助你更好地理解接下来我所要说的几个东西。
OCL语言调研
OCL(object constraint language)是对象约束语言，用来进行对象的约束定义，是形式化的无二异语言。其由1995年Warmer等人在IBM设计成功并开始使用。OCL主要用于在建模时作为图形符号的补充,含有约束,前置条件,后置条件等。不变量是在属性的生命周期内保持为真的规则，前置条件是一个操作被调用时需要满足的约束，即满足规格要求。后置条件是操作结束后一定为真的约束，即完成了什么操作。监护规则是对象从一种状态转变为另一种状态前值必须为真的约束。
OCL与JSF的相同点在于他们都是形式化的约束语言，在程序中进行无二义的逻辑约束。结构上也具有相似性，OCL主要包括的不变量，前置条件，后置条件，监护规则分别对应JSF对应着repOK()，REQUIRES，EFFECTS和MODIFIES。
而他们的不同点在于作用的时间不同，OCL主要是在编写程序前，理论建模时刻对每个类进行明确的约束，而JSF主要在功能实现前进行约束以确保程序逻辑实现正确。
第十四次作业模型
UML类图
UML时序图
UML状态图
学期小结
四个单元模块知识点联系
第一单元主要是java入门到面向对象设计。从多项式计算到傻瓜电梯的练习，使我们学会并巩固了面向对象设计的思维，也让我们意识到高内聚低耦合的对象设计的重要性。
第二单元是从面向对象设计到多线程的转变。在这个单元中我们主要扩展了电梯的功能并实现了多线程电梯，线程的安全问题和如何合理的利用线程的同步和互斥成为了这一单元的关键。
第三单元第一次引入规格化设计，在我们对于面向对象设计和线程设计有初步了解的基础上，使我们学会了如何增强自身代码的可读性。同时也教会我们使用前置条件对方法进行约束，从方法的层面去实现程序的正确性。
第四单元引入自动化测试，基于输入实现软件生成的自动化覆盖测试，可以在一定程度上帮助我们更好地去论证程序地正确性。
梳理与进步
程序功能上，在设计上更加明确各类地分工和均衡分配类的任务，并且程序更加地向SOLID原则看齐。
程序测试上，从早些的编造多样例覆盖到后来的针对分类树设计测试样例，最后到从方法的正确性角度测试程序。
工程化开发理解
在我看来，工程化开发是不同于简单的程序撰写的，从简单的作业到需要许多人一起合作的项目，其中代码的可读性和规格极为重要。同时，对于自己程序的测试也尤为关键，因为整个项目可能会因为你的一个bug而出现很大的漏洞。
期望与建议
期望课程设计上可以增加对于多线程的方面的教学，感觉目前的指导书和ppt并不能很好地满足学生的学习需要。同时，希望在早期几次简单的作业中加入规格化设计，这样可以让同学们从一开始就可以了解到规格化设计的重要性，并且可以从规格的学习中了解到程序设计的重要性，而不是简单的埋头写。