一、测试与正确性论证的效果差异及其优缺点
第十三次作业中我们学习并使用了Junit单元测试框架对我们在第三次作业中编写的具有捎带功能的ALS电梯进行测试。当时没有对于捎带有很好的理解，加上自身代码基础的问题，代码十分冗长，有的类非常长。在进行Junit测试时，在测试长类的时候覆盖相当困难，对于每一个分支的覆盖更是难上加难，为了完全覆盖，我构造了很多的测试用例，虽然十分麻烦，但正是测试用例的完善让我找到了我的问题所在，成功找到并排除了当时的很多bug，最终完整的完成了要求。
第十四次作业中我们学习了通过正确性论证的方法对程序进行了正确性分析，使用的程序依旧是第三次作业的电梯程序。主要内容是通过前面学习的JSF规格，依照规格对程序每一个类的输入进行划分，对于每一个划分出来的小分支，都要通过代码运行逻辑验证其满足规格的后置条件。JSF各条件明确且可验证的基础上，通过每一个分支覆盖所有输入可能，就能够分析代码的漏洞，并且对规模较大的方法进行拆解或重构，达到优化代码的目的。
综上，其最本质差异在于，单元测试不管代码内部的构造，只要输入的结果和运行的预期相同，就能认为正确，即为黑盒测试。而正确性论证则是从代码的具体逻辑入手，不看运行，深入代码的实现，一步一步剖析，是为白盒测试。
具体优缺点来看，单元测试能够自动化，只需构造测试集就能自动运行并看到结果，非常方便，但是问题在于测试数据很难做到绝对完备，也就是说这样的测试很可能仍然会留下bug。正确性论证能够从代码实现来分析，如果能够论证，那么可以保证代码能绝对正确的完成规格的要求，即能保证代码功能的正确，缺点相当明显，论证过程过于复杂费时，同时如果要重构代码则再次论证也同样复杂。
二、OCL语言与JSF
OCL是一种描述UML建模细节的对象约束语言，它是UML标准的一部分。OCL是一种声明式语言，大部分表达式执行后会返回一个布尔值 。
OCL语言和JSF的相似之处有
都可以描述不变量、前置条件、后置条件
都是基于数学中的谓词逻辑，有一个形式化的数学语义
理想情况下，都无二义性
不同之处有
OCL语言是基于UML类图的，而JSF是基于代码本身的。
OCL是一个类型语言，任何表达式的值都是属于一个类型的。这个类型可以是预定义的标准类型例如Boolean或者Integer，也可以是UML图中的元素例如对象，也可以是这些元素组成的集合，例如对象的集合、包、有序集合等等。 但JSF中并没有对这一点做出要求。
三、UML
UML类图
UML时序图
UML状态图
四、总结
第一单元，从零开始学java——类与对象。第一单元有三次作业：多项式加减、单傻瓜电梯、单捎带电梯。训练主要是Java基础编程训练，训练同学们面向对象编程的能力，让同学们熟悉和掌握面向对象编程的方法和技巧。在这一单元，用面向对象的方式解决问题是难点所在。
第二单元，进阶的java——并发与安全。这一单元三次作业：多线程电梯、ifttt、出租车调度，难度飞跃。多线程的首次引入、指导书的繁杂、调试的不便、互测的博弈、线程安全的迷之bug。这一单元，线程安全问题是难点所在。
第三单元，规范的java——规格化与设计。这一单元从第七次作业出发，代码上每次增加一点功能，主要考察规格化设计。难点是写好规格、完成好规格。
第四单元，正确的java——测试和论证。这一单元依次介绍了两种测试方法，junit为代表的黑盒测试，正确性论证为代表的白盒测试。这一章的难点在于将之前代码规范化并且验证。
联系：已经明显了，课程让同学们循序渐进的了解java，从初识到进阶到规范，最后回头论证，是一个完备的训练体系，条理清晰。
进步
最大最明显的自然是对java语言的使用，从0开始一步步到了现在。
然后就是不同于以往c的面向过程，面向对象的思维方式有着不同的体会，从最初的不适应到现在能有深刻认识。
多线程是一种很奇异的体验。
测试方法从无脑撞测试样例到现在有条理的对代码进行分析，思路更加开阔，方法更加多样。
代码规范意识更强，最初即使是自己的代码，过了一周就可能不知道是写的什么了，导致作业上困难重重，将代码规范化，既有助于自己debug，也对工程化编程更有帮助。
对工程化开发的理解
工程化开发往往是给予团队的协作，那么最关键的就是良好的沟通。在保证代码正确性的基础上，对可读性和规范性有很高的要求，这是合作交流的重要基础，能有效提高交流效率，否则一个人代码能力再强别人看不懂也是白搭。如果有能力，尽量将代码简洁，这样能对交流的成本进一步降低。
建议
关于第七次作业的设置，出租车问题的编程会在规格出现后整个单元连续用3次，而第七次作业编过后，再到第9次作业开始来写JSF，很大程度上会有惯性思维，以及代码会直接套用，就违背了规格先写再写代码的初衷，效果会降低，但是直接第九次作业写出租车问题又要写JSF工作量似乎太大，希望课程组能够找到具体的调整方法。