一、测试与正确性论证效果的差异及其优缺点
在第十三次作业中，我们使用了JUnit单元测试框架对我们在第三次作业中编写的捎带电梯程序中的每一个方法进行了测试。捎带电梯程序在经过了互测之后，已经是一个比较完善的系统，但是通过大量细致的单元测试，仍能从程序中寻找到一些逻辑漏洞甚至错误。通过观察每个方法的语句和分支覆盖率，可以比较直观地看到自己的代码是否每一行都有其价值。在写第十三次作业的过程中，我不止一次遇到了这样的情况：在针对某一个复杂的方法设计大量测试用例，甚至用程序自动生成随机测试样例，都无法对某一条语句或者某一个分支做到100%的覆盖。这个时候，我就会重新检查这个方法的实现逻辑，判断这条语句或者这个分支是否真的有存在的必要。很显然，细致的单元测试有助于我们优化和完善自己的代码。
而在第十四次作业中，我们采取了正确性论证的方法对同一个捎带电梯程序进行了正确性分析。通过对JSF的后置条件进行划分，将一个方法所需要处理的所有情况分为几种小的分支，然后对这些小分支逐一审视代码的实现是否满足了JSF的后置条件。在JSF后置条件明确且可验证的基础上，正确性论证可以使我们重新审视自己的代码，细致地分析其实现逻辑，并确认自己是否覆盖了每一种可能的情况。由于第十四次作业是在第十三次作业完善后的程序之上完成的，因此正确性论证没有帮助我找到代码中的逻辑漏洞；但它驱使我完善自己的JSF后置条件，并且对规模较大的方法进行拆解或重构，以达到可进行正确性论证的目的。从这个角度上来讲，正确性论证进一步优化了程序的可验证性。
单元测试和正确性论证的本质差异其实用一句话就可以概括：单元测试是黑盒测试，而正确性论证是白盒测试。
在构造单元测试的测试样例时，测试者可以完全不知道程序的具体实现细节，机械化地生成测试数据，并根据方法的规格判断方法的实现是否正确。它的好处是简单粗暴快速有效，经过大量测试数据的轰炸，代码中最细微的漏洞也可以被揪出来并得以修正。此外，单元测试对代码的重构具有奇效。如果没有自动化的单元测试，重构代码的时候就需要不停地去手动验证之前的测试样例，一旦发现问题，修改之后又要重头跑，既浪费时间，又容易出错。单元测试有助于程序设计者以自动化的方式去验证程序的正确性，这是正确性论证所不具备的优点。但是，单元测试也有其缺陷：由于它是黑盒测试，从概率的角度上讲，无论测试数据再怎么完善，总会有漏网之鱼的Bug出现。换句话说，在程序有一个良好的设计且规格完善的前提下，单元测试可以保证程序的正确率达到99%以上，但无法确保100%正确。
正确性论证与单元测试不同，它是白盒测试，这意味着测试者需要深入代码的实现，去逐个论证实现与规格上的不同之处。这个过程比较繁琐，而且对重构极不友好，一旦代码发生较大的变动，许多方法的正确性论证就要重写，造成很多额外的麻烦。但是，这些麻烦换来的好处就是，一个被正确设计了的且规格完善的程序只要完成了正确性论证，就可以从逻辑上确保100%的实现正确性，其保证力度要大于单元测试的保证力度。因此，对于一些不再需要进行修改的方法，进行正确性论证是比单元测试更为稳妥的选择。
在实际的工程中，我认为应以单元测试为主，正确性论证为辅。因为需求总是在不断变动的，单元测试的简便和高效适合更现代软件工程的开发流程。而对于那些比较重要的核心算法代码（即不会随需求更改而变动的代码），应进行正确性论证，以确保逻辑上的100%准确。
值得注意的是，无论是单元测试还是正确性论证，其有效的前提都是程序的设计是合理且正确的，各个类和方法的规格也都已经完善。没有规格的代码就像没有标准答案的考试卷，学生答起来群魔乱舞，老师判起来无从下手。单元测试和正确性论证都是必要的，但这并不代表有了它们就可以万事大吉。在软件开发环节的最开始就做出合理的设计，并且撰写好相应的规格，单元测试和正确性论证才能发挥其最大作用，为提高程序的正确性带来价值。
二、OCL(Object Constraint Language)语言与JSF
OCL语言是约束(Constriant)语言和查询(Query)语言。一个约束就是对一个（或部分）面向对象模型或者系统的一个或者一些值的限制，UML类图中的所有值都可以被约束，而表达这些约束的方法就是OCL语言。在UML2标准中，OCL语言不仅能够用来写约束，还能够用来对UML类图中的任何元素写表达式，每个OCL表达式都能指出系统中的一个值或者对象。因为OCL表达式能够求出一个系统中的任何值或者值的集合，因此它具有了和SQL同样的能力，因而OCL也是一种查询语言。
OCL语言的基础是数学中的集合论和谓词逻辑，并且它有一个形式化的数学语义，但是它并没有使用某种数学符号。因为虽然数学符号能够清晰的、无歧义的表达事物，但是只有极少的专家可以看懂。所以数学符号并不适合用于一个广泛应用的标准语言。自然语言是最易懂的，但它却是含混不清晰的。OCL取了自然语言和数学符号的折中方案，使用普通的ASCII字符来表达数学中同样的概念。
OCL是一个类型语言，任何表达式的值都是属于一个类型的。这个类型可以是预定义的标准类型例如Boolean或者Integer，也可以是UML图中的元素例如对象。也可以是这些元素组成的集合，例如对象的集合、包、有序集合等等。
OCL是一种声明式(Declarative)语言，表达式仅仅描述了应该去做"什么"，而不是应该"怎样"去做。因为OCL是声明式语言，所以UML中的表达式被提升到了纯建模的领域，而不必理会实现的细节和实现的语言。
OCL起源于1997年BIM公司为响应OMG的"面向对象分析和设计标准"征求稿所提交的"对象时间限制提议"，OCL是该提议的部分内容。用OCL可以描述四类约束，分别是不变量、前置条件、后置条件和监护条件：
1）不变量是在属性的生命期内一直保持为真的规则。
2）前置条件是在一个操作被调用时必须为真的约束。它是一个断言，不是可执行语句。
3）后置条件就是在操作完成时必须为真的约束。它不是可执行语句而是断言，必须为真。
4）监护规则是在对象能够从一种状态转变为另一种状态前其值必须为真的约束。
每一个OCL表达式都必须赋予一个明确的上下文来定义参考基准。在模型中的任何一个元素都可以定义为一个上下文，例如类、属性、操作和关联。一旦我们定义了上下文，就可以开始定义约束表达式饿。OCL是一种声明式语言，大部分表达式执行后会返回一个布尔值，也有一些表达式会用来选择一个单一值或者一个对象/值的集合。
可以看到，OCL语言和我们在面向对象课程中所学到的JSF具有相似之处。不变量、前置条件、后置条件这些我们已经耳熟能详的概念在OCL和JSF中都有体现，其所代表的含义也都大致相同。OCL中的监护条件则有点类似于JSF中的repOK方法（但并不完全一致），即系统状态只要满足相关要求，就可以进行任意满足规格的调用。通过对这些约束的断言，我们得以判断一个方法是否被正确调用或者是否被正确实现，相当于为一张空白的试卷制定了规则和答案。有了这些规则和答案，我们再去具体撰写代码实现的时候，就有了相应的依据，可以自行判断出实现是否正确。此外，它们还可以帮助我们撰写高质量的单元测试和正确性论证。
不同之处在于，OCL语言是基于UML类图的，而JSF是基于代码本身的。从严谨性程度上来讲，JSF也更高一筹，因为正如上文所说，布尔表达式（以集合论和谓词逻辑为基础）是最严谨的表达，其带来的约束的严谨性远胜于自然语言，且适合进行自动化验证。但是，形式化的数学语言并不适合所有人阅读，而且一些较为复杂的逻辑可以用简单的自然语言描述出来，但绝对无法用简单的数学语言去描述。因此，OCL和JSF各有其适用范围，两者的缺点正好是对方的优点。在工程开发中，二者互补为佳。
三、单捎带电梯系统的UML表示
四、学期训练总结
1. 四个单元模块知识点之间的关系
第一单元有三次作业：多项式加减、单傻瓜电梯、单捎带电梯。第一次作业的难度极小，主要是为了让同学们初步接触Java编程，并将思维从C语言的面向过程转为Java的面向对象。第二次作业的单傻瓜电梯稍有难度，相比于多项式加减，同学们需要设计并实现的类变多了，大部分同学在这次作业中第一次体验到了多个类协作带来的面向对象编程体验。第三次作业的难度陡然增加，指导书变得复杂了许多，算法也比较难以实现。尤其是同学们在写单电梯的时候还需要考虑之后的多线程电梯，因此写的时候小心翼翼、举步维艰，生怕后面还需要重构（然而事实证明，多线程电梯还是需要大规模重构…）。
第二单元可以说是整个课程体系中最难的一个单元。多线程的首次引入、指导书的繁杂、调试的不便、互测的博弈，这些元素使得这三次作业的难度陡然增加。第五次作业的多线程电梯中，同学们需要通过多线程完成三部电梯的协作，并在捎带算法的基础上增加最小运动量原则。这些算法和之前的差别不大，难点在于多线程对调度器实现方法的影响。第六次作业是文件监视器，是指导书改动最频繁的一次，绝对难度并不大，复杂之处在于仔细理解指导书，并完成一个线程安全的设计。第七次作业的出租车调度是一系列作业的开始，这次作业中首次引入了设计原则，通过满足这些设计原则，同学们可以在之后的增量设计中取得工作量上的减轻。
第三单元主打JSF。第九、十、十一次作业循序渐进，逐步引入方法规格、类规格、带有继承的类规格，让同学们可以通过完善规格，掌握做出一个良好设计的方法。这三次作业的难度不大、算法简单，但是要想写好JSF还是需要下一定的功夫。
第四单元是测试与论证。一个程序如果没有正确性，那就不配称之为一个程序，第十三次作业的JUnit单元测试和第十四次作业的正确性论证是两种增加程序正确性的方法，通过这两次作业对第三次作业单捎带电梯的检查，同学们基本掌握了测试和验证自己程序的方法，这种方法在之后的编程生涯中大有裨益。
这四个单元有一个清晰的主线：熟悉面向对象 à 多线程编程 à 设计与规格 à 测试与验证。这条主线是从一个对面向对象完全没有概念的编程新手到能写出1000行具有优良设计风格的面向对象代码的人所必经的学习道路。四个单元之间循序渐进，却又藕断丝连，对同学们而言有着很大的训练价值。
2. 我的进步
在面向对象课程中，我的主要进步可以用一句话来概括：从拿到需求（题目）就开始无脑写代码，变成了先思考再编码。我觉得大二整个课程体系（包括但不限于计算机组成、面向对象）都是在训练我们设计与实现分离的编程风格，事实上经过这一年的训练，我的设计能力和编码能力确实有了长足的提高。
此外，还有一些小的方面的进步。例如，以前我从未接触过多线程编程，也没有使用过Java的反射，面向对象课程的作业让我熟悉并掌握了这些很有用的编程工具。
3. 对工程化开发的理解
我并没有参与过真正的工程化开发，因此接下来这一小节的内容都是基于我的想象。
我理解的工程化开发，重点在于协作。现代大型的软件工程规模已经大到了绝对不可能仅靠一个人单枪匹马就能完成开发，因此多人协作就显得尤为重要。当许多人一起完成一个大型项目的时候，由于每个成员的能力不同、对项目的理解也不同，因此如何进行良好的沟通（包括语言层面的沟通和代码层面的沟通）成为了一个很大的问题。面向对象这门课程所教授的规格化设计就是解决沟通问题而进行的一个尝试。类的设计者通过规定前置规格来约定使用者的输入参数范围，通过撰写后置规格来提示使用者类和方法调用后的作用；类的使用者通过遵循前置规格来获得满足后置规格的调用结果，通过反复调用repOK方法获得类是否能够正常工作的反馈。
"协作"这个词的内涵是丰富的。为了沟通方便，完善的注释和优秀的代码风格是必需的，各种设计原则的满足是必须的，规范撰写的过程规格也是必需的。如果没有这些，一个人无法理解另一个人的想法，无法对代码作出修改和重构，即使是代码撰写者自己，也会在一段时间之后，忘记之前代码的设计思路。因此，在工程化开发中，为了沟通和协作的需要，更多的时间应该花在规划、设计和测试上，真正的编码实现只占整个工程的一小部分。
工程化开发和自己做一个小项目完全不一样。在自己的项目中，任性没有关系，甚至有时候任性能够来带来更好的创意；然而在工程化开发中，任性只能给整个团队带来灾难。
4. 对课程的任何期望或建议
希望能够取消后面三次的出租车作业（即第三单元的三次以JSF为主要训练目的的作业），改为一个从零开始的、先撰写规格再完善代码的循序渐进的项目。在现有的课程体系中，同学们接触JSF的方式是通过先写代码再补充规格的方式，这使得大部分同学难以体会到规格化设计对于一个工程项目的重要性。如果能够通过一个系列作业，让同学们完整体会先设计再实现的过程，想必"设计无用论"的想法会少很多。
此外，在互测制度上，建议再完善一下JSFTools，为JSF制定一个统一的规范标准，以避免互测双方对JSF标准的理解不同而引发的争论。
最后，希望面向对象课程能变得越来越好，而不是让越来越多的人去讨厌。