测试与正确性论证的效果差异及优缺点
测试实际上就是对程序进行的一种黑箱测试，利用各种各样的测试样例去检验程序是否能够给出正确的结果。其中的单元测试则是将整体的测试拆分成单元来进行，但其仍然躲不开黑箱测试的形式。而正确性论证虽然也是从各个方法入手，但其并不是盲目的对比输入输出是否一样，而是从逻辑上梳理某个方法运行过程中仅可能出现的输入（即前置条件）和针对这些输入仅可能给出的结果（后置条件），从而在确保各个方法实现均正确的情况下将其组合起来成为一个正确的系统。
从效果上来讲测试由于并不能穷举所有的情况，而正确性论证我认为实际上是对各种情况的抽象和归类，从而将无穷变为有穷，其效果也明显优于测试。但正确性论证如果要梳理清楚各种逻辑的关系，其复杂程度要高于测试很多， 因此做起来也相对复杂，测试只需要设计各种测试样例并且自动运行查看结果即可，相比而言较为简单。
OCL调研及与JSF的异同
OCL (Object Constraint Language) 即对象约束语言，是一种指示用户建模系统中的限制方式，它是UML可选的附加内容，可以用来更好的定义对象的行为，并为任何类元指定约束。
OCL是一种精确无二义性的语言，并且是一种规范说明性语言，能够用来约束UML图中的对象。
与JSF的异同：
相同：
均使用了数学的方法（谓词逻辑、集合论）来表达对对象和方法的约束，都采用了自然语言和数学符号折衷的方式
均是一种声明式的语言，即内容中不包含具体实现
都包含前置条件和后置条件的声明，也都包含不变式相关逻辑
不同：
OCL中没有JSF的MODIFIES，但多出了“监护规则”。除此之外OCL非常注重类型的声明，并且细化了各种容器，相比之下JSF均抽象为数组来表达了。
第十四次作业类图、顺序图、状态图
学期总结
四个单元模块知识点之间的关系
第一单元我认为主要是初步认识面向对象思想，掌握类属性方法等元素以及继承、多态等OO的基本思想，顺便学会如何使用Java编写OO程序。第二单元主要面向OO当中的多线程编程，在前一个单元的基础上利用面向对象的方式编写多线程程序。第三单元主要是JSF的引入，以及设计方面的更高级要求（如SOLID、规格）。第四单元则是对于测试和正确性论证的学习，即一个程序写到最后要确保写的是对的。
这四个单元我认为前两个单元主要更侧重编程技术方面，实际上学习多线程编程除了掌握并行的思想外，更重要的其实是怎么在多线程如此混乱的情况下让程序跑出自己想要的结果（想起了OS中的互斥和同步的关系），因而技巧方面更重一些。而后两个单元则更侧重设计以及编程之后验证的部分，前者让我们养成良好的设计思想，我认为规格化的开发思想在程序规模增大的时候才能体现其优势；而后者让我们确保了自己程序写的是对的，能够经过各种各样的检验。
自己的进步
一个学期以来写了多项式、电梯三部曲、IFTTT、出租车四部曲这么多程序，可以说进步应该还是有的。
从设计和代码质量上，一开始代码耦合高，第一次ALS电梯一个方法有200行，到后来程序逐渐变得层次清晰，最后第13次和14次作业对电梯进行了解耦，将原先200行的方法拆分成很多个，每个的行数都较短。原先因为DRY做的不好，重复代码较大导致经常出现改一处忘了改另一处的情况之后也变得很少了。
虽然第一单元的程序几乎没什么bug，但设计思路方面的不清晰导致多线程部分有所翻车，但在对程序的构思逐渐形成合理的模式后，这种情况在出租车有了很大改善。
对工程化开发的理解
我是从大二才开始听说“工程化思想”这一词的，印象最深刻的实际上也是上学期的计组，老师不断的强调“工程话思想”。实际上工程化思想我认为只有当程序需要达到一定规模时才能看出其优势，无论是这学期OO到最后代码量很大的出租车还是上学期完成的计组实验都可以说明这一点，而这两者相比于真正的工程而言更是小巫见大巫。
虽然到现在为止我还没有接触过真正的工程化开发，对于作业也仅仅是利用了一点“思想”而已，因此我的理解还只能停留在空想的阶段。我理解的工程化开发，首先是一种模块化的设计，整个程序是由多个模块构成的，这些模块满足所谓的“高内聚、低耦合”关系，单独来看虽然不能做什么但组合到一起才能完成很复杂的工作。其次作为一个“工程”，必定是一个相对长久的概念，因此需要很多个人“前仆后继”的进行努力。因此在工程化开发中我认为规格很重要。如何让大家编程的点子统一起来，同时让大家编写的一个个”模块“最后能顺利的组合在一起是一个需要重视的问题。规格设计以及接口这一概念在其中充当了非常重要的角色。
对课程的期望和建议
1. 在写作业的时候很多问题我都是从同学的口中得知在”他们班的群里“助教说了什么什么要求，很多时候这些要求没有被通知到，也出现了最后申诉中两人互飙微信群截图的情况。希望可以有一种统一的要求通知机制（比如对于各种问题能及时梳理到issue），能够统一口径并且减轻助教答疑和同学们追问的压力。
2. JSF方面首先我感觉可以借鉴一下OCL语言，例如其中的各种容器。其次课件中经常使用多项式以及数组等等来举例子，在这些方面的确JSF可以清晰的表达规格，但对于出租车等复杂逻辑而言没有很好的参考价值。希望课上能多一些较为复杂的例子。
3. 多线程其实在这个课程中的位置稍显尴尬，的确很重要，但也导致学习曲线较为陡峭。本学期中期OS课上我们也接触了很多并发相关的概念，其中PV操作讲的那些并发经典例子其实对多线程理解有不少帮助。第一次多线程电梯之前那节多线程的课对于多线程电梯来说有点“不够”，导致多线程电梯写的云里雾里。希望在多线程的起步教学这方面可以增加一些内容帮助理解。