一、测试与正确性论证的区别
从哲学的角度来说，正确性论证与测试的关系就像理论与实践的关系一样。
使用测试的方法检验程序正确性确实是一个非常方便可行且广泛运用的方法。可以通过几个简单或复杂的测试样例，迅速地校验程序主要逻辑是否正确，运行结果是否符合预期。但是对于较为复杂的问题来说，测试样例很可能并不能覆盖所有的情况，因此我们曾经引入代码覆盖率和分支覆盖率的概念。但是在操作过程中我发现，即使某个不完全的测试样例代码覆盖率达到100%，分支覆盖率高于95%，它仍然并不一定完全检验程序的逻辑是否正确，即使结果符合预期。因此我们很难通过测试样例说明程序一定正确，即使我们使用了脚本生成等自动化测试方法，仍然不能全面地测试程序的逻辑是否完全正确。因此测试这样的方法有着其便捷性，也有着其局限性。
正确性论证是一个全新的思路，我们把程序的逻辑构造成分支的形式，通过规格总结出在各个分支下程序的预期表现来从宏观的逻辑层面上论证程序是否正确，不去关心程序运行过程中如何实现，只需要满足规格提到的前置条件和后置条件即可认为程序正确。但是对于复杂问题，构建出程序的逻辑分支便已经十分吃力，程序的复杂逻辑很可能在分析的过程中遗漏一些错误，因此这并不是一个万全的方法。
我们在实践中，应该结合二者进行测试，虽然耗费时间，但是在对程序认知较为深刻的情况下，自然更容易思考到比较偏僻和少见的逻辑问题。
二、OCL语言
OCL语言是对象约束语言，与JSF相似，同样拥有着前置条件和后置条件，但是没有JSF中的Modified属性，有类似的不变式。还有叫做监护规则的约束，即在对象能够从一种状态转变为另一种状态前其值必须为真的约束。
OCL语言和JSF一样，都只关心方法或对象在运行前后的属性状态，不关心具体的实现过程。
三、第十四次作业总结
以上是第十四次作业的UML类图。
以上是第十四次作业的时序图。
四、学期总结
本学期我们首先学习了面向对象语言的初级应用，完成了一个看起来很不面向对象的Java程序——多项式计算，这个程序由于功能简单，导致其类的功能过于集中，Main类用于录入信息，ComputePoly类用来计算多项式加减，确实是难以感受到Java面向对象程序与传统面向过程程序的区别（除了程序中多了几个class关键字）。当然现在看来，这个程序还可以写得更面向对象一点，更完美一点。但是对于一个什么都不懂的初学者来说，用这个作业入门且由于设计需求中对输入的严格要求，大家往往会把注意力集中在java的基本语法学习和正则表达式在Java中的运用之中，反而忽略了面向对象程序的关键。愚以为，这个作业可以进行一些改进以更加地偏向面向对象教学，不过考虑到由于需要公测进行测试，且规范输入格式对之后电梯程序的铺垫作用，设计出这样的作业已经是非常合理了，且暂时也难以想到兼顾二者的作业设计，毕竟对于当时的我来说，面向对象还是一个非常抽象笼统的概念，是需要一个学期的学习才能正确认知的。
随后我们完成了两次单线程电梯，第一个是傻瓜式电梯，之后我们运用了学到的类的继承，将其升级为有一点点智能的可捎带电梯。到这里，我们已经可以管中窥豹地初步认识到Java面向对象中一大特性之继承的作用以及好处，同时对单线程编程也是较为熟练。
之后我们便愉快地进入了Java多线程的世界，我们首先再次升级了之前的稍微智能一点的小垃圾电梯，将其改造为非常小可爱的三部电梯同时工作，并且直接进入了多线程阶段，可以真实地模拟时间，简直是太酷了！
这三次作业让我们发现，在功能升级的时候，总是有一些其他无关类（如Floor类）的代码由于一些不可言状的原因必须进行修改，这是怎么回事！明明很厉害的面向对象怎么会有这种情况出现！难道是我做错了什么！原来随着需求的修改，程序的逻辑有了很大的变化，之前在楼层类中使用了一些属性来记录相应的请求，而在多线程电梯里又用不到了，导致这部分逻辑在方法中冗余，才需要大量的修改甚至是重构。此时我们发现了，类的抽象化做的非常的不好！楼层就是楼层嘛，楼层有楼层的功能，为什么还要用来记录请求信息呢（其实是因为要打印输出），记录请求信息意味着类之间的耦合性变高了，这也就是我们必须要修改除去scheduler类之外的其他代码的原因。
当这一作业告一段落，我们完成了一个用作过渡的，用来帮助我们学习多线程的线程安全和同步控制的作业——文件系统。在这次作业中，我们学习了诸多线程安全的手段（有且不仅有sleep(200L), sleep(500L)和sleep(1000L)），极大地提升了自己在线程同步控制上的造诣。
在之后的Taxi作业，我们早早就听说了本次作业将有多次升级，因此我在实现时很认真地思考自己的程序，如何让自己的程序变成高内聚低耦合的神奇存在。又在线程控制上有了很深的认知，使这次作业的线程同步的矛盾从设计层面上被尽量避免。同时又完成了需求提到的并不丰富的功能，其中最困难的部分可能是重新写一个好用的最短路径搜索以替代原本GUI中提供的特别占内存且特别慢的方法吧。
之后不论是为道路添加流量还是添加红绿灯还是设置VIP出租车，都极大地体现了一个良好的程序构思是多么的有意义，添加流量时由于要修改map类的逻辑，包括最短路搜索，导致需要写不少代码，之后的红绿灯几乎只修改了两三个方法，修改了十几到几十行代码就解决了这个问题。而可追踪出租车更是完美的体现了面向对象程序中继承的优点，程序的其他部分对可追踪和普通出租车的处理完全没有区别，却可以很好地完成功能需求。再加上某个选修课学到的c++面向对象的相关知识，到这，我觉得面向对象程序中继承的运用以及好处已经被我掌握个大概了。
从Taxi第二次作业开始，我们引入了全新的程序设计理念——规格，这个东西可以很好地统一程序员之间的交流语言，也可以为自己的程序设计提升便利。这一部分与我们之后的几次作业有着极大的关联。
之后的几次代码量非常小的作业中，我们先后接触了JUnit单元测试、程序正确性论证等概念，这两个概念令我对之前蠢笨的测试方法感到十分羞愧，想起当时百度的时候也曾经看到JUnit的使用方法但由于懒惰并没有深入学习，导致刚开始在对程序测试时，几乎都在使用复制粘贴按回车大法。但是代码量小并不代表作业更轻松，虽然当时的我在身体及意识上对它们都有些不重视，但是在实践过程中，发现当初写的程序简直是太难以接受了，将这样的程序整理出合适的规格实在是过于繁琐。因此，迫不得已地修改了一小部分代码使程序变得好看一点。又由于在第二次电梯作业中对其非常的上心，记得当时很多的逻辑结构，因此很容易就构造出了符合条件的测试集。虽然由于逻辑的复杂，在正确性论证的过程中碰了钉子，但总体来说还算比较顺利。
从我个人的角度来看，这一路走来，我的工程化能力有着比较大的提升和进步，对面向对象的学习也是非常认真。因此非常感谢OO课程组为我们精心设计的关卡，非常感谢助教在这一过程中对我们的帮助。就我个人来说，相信如果没有OO的闯关机制来辅助我的学习，单纯通过上OO理论课，然后随便布置一些作业的话，我很难对OO这门课的认识有如今的程度。
原文地址：https://www.cnblogs.com/SephyFine/p/9223940.html