测试与正确性论证的效果差异
测试，或者说用断言进行黑箱测试，用大量的数据进行“覆盖性测试”，目的是当分支覆盖率达到100%也就是理论上来说所有可能的输入都已经测试过了，而输出结果均是正确的，那么我们理论上可以说这部分程序是没有问题的。这种测试方法的好处就是，问题暴露得十分明显，某一组数据错了，就知道问题发生的情况是什么了，复现性也很强。其实平时我们自己debug的时候用的就是这种方法，只不过那时我们测试量比较小，并没有做到全覆盖，而是向着我们感觉可能会出错的方向进行测试，导致测试以后仍然感到不安，害怕仍然存在着某些bug自己没有发现。现在有了全覆盖的测试，这种方法比较好实现，效率也比较高，只是不可以完全验证程序逻辑的正确性。
正确性验证，就是通过分析需求写出正确的规格，然后论证程序在规格的任意划分下，都符合规格所要求的过程。这种验证方法偏向于验证程序的思路、逻辑是否正确。严格按照这种方法执行，可以验证程序是否有按照我们所希望的那样执行，但由于是理论上的分析，所以需要严谨细致的推论，因此可能会比较耗费时间。
无论是这两种哪一种测试方法，都让我学会了如何准确性较高的测试自己的程序（发现更多的bug），都使我受益匪浅。
OCL语言和JSF规格的对比
对象约束语言，即OCL语言是一种形式化语言，它主要用于表示UML模型中施加于模型上的约束。OCL具有如下特点：
1、OCL是一种精确的，无二义性的语言。
2、OCL是一种规范说明性语言，所有有关实现的问题都不能用OCL来表达。
3、OCL是一种纯表达式语言，它是具有没有任何副作用的申明性语言。
4、OCL是一种类型化语言，即OCL中的每一个表达式都是具有类的。
5、OCL不是一种程序设计语言，不能用OCL编写程序逻辑和控制流程。
它和JSF规格的相同点在于它们都是形式化的约束语言，在程序中唔二义性，结构上也具有相似性，OCL主要包括的不变量，前置条件，后置条件，监护规则分别对应JSF对应着repOK()，REQUIRES，EFFECTS和MODIFIES。
他们的不同点在于作用的时间不同，OCL主要是在编写程序前，理论建模时刻对每个类进行明确的约束，而JSF主要在功能实现前进行约束以确保程序逻辑实现正确。
第十四次作业模型图
1. 类图
2. UML时序图
3. 状态图
课程总结
1. 四个单元模块知识点之间的关系
第一章的多项式计算和傻瓜电梯，主要是为了使我们从面向过程编程转变到面向对象编程，在写代码的过程中体会面向对象的思想。
第二章主要是线程安全的学习，引入线程的概念，运用多线程来提高工作效率，同时也就引入了线程安全的问题，如何保证进程互斥和资源共享是我们本章需要思考的问题。
第三章主要是抽象和规格化设计，通过写规格来增强代码的可读性、可移植性，让我们写的代码可以为他人所用。
第四章是测试与论证，随着程序规模的逐渐增大，人工测试难以保证程序的正确性（其实哪怕程序规模小人工测试也很难完全覆盖），所以无论是自动化测试还是正确性论证，都是为了通过理论层面论证程序的正确性。
2. 梳理与进步
程序肯定是写得比以前好很多，无论是在程序结构还是可读性上，从一开始的数量少但功能贼多的类（GOD类）到一点点每个类的功能相对均衡，各个类可扩展的空间也多了不少。可读性上，命名风格向大佬们学习基本也能做到精简且明晰，同时也按照课程要求写了详细的JSF（虽然有些还是很长很长很长很长），可读性改观了许多。
测试方面，从一开始的只能靠乱想例子，寝室共享一波数据，到现在的覆盖性测试，还有正确性论证，使得测试的过程更加有条理，结果更加可信。
3. 对工程化开发的理解
emmmm工程化开发就是很多很多很多人一起写代码，所以自己写的代码就会被自己的队友所使用，因此本着“以人为本”的思想，我们就要让自己的程序可以很方便的被别人使用，就像一个很标准的、契合的齿轮，可以帮助整台机器运转，与其它部件共同合作完成各项功能，而不是因为自己的不契合而导致整个团队延缓开发速度甚至项目失败。
4. 期望与建议
首先感谢老师与助教这一学期以来的辛勤付出，使我在编程能力和思想上都有了很大的提升。期望的话，希望可以明确一下教学目标，感觉有些要求本身就相悖，比如说，一方面指导书并为对所有情况进行详细的要求说明，是为了锻炼大家理解自行设计的能力；而另一方面，由于互测这种竞争机制，同学又会在issue或是助教群中对每一种详细的情况应该如何处理进行询问，希望得到官方的回答，以此来规范自己或是挑别人的bug。窃以为，如果真的为了提升自行设计的能力，不如就不要在指导书已经发出以后，再进行各种要求，否则这和一开始就规定好有什么区别？还大大增加了学生与助教、助教与老师之间交流的时间成本。如果说需要进行某些硬性要求，就在一开始的时候将指导书写清楚，毕竟指导书永流传，一次修改福泽学弟学妹。