一、论述测试与正确性论证的效果差异，比较其优缺点
程序的正确性论证是用户提出需求后，开发人员根据用户需求进行分析，得到需求规格，论证所写的程序程序是否符合规格的过程。因为规格往往是布尔型或自然语言，对程序员来说并不如代码和测试数据直观，且工作量巨大。但相应的，好处是对代码整体进行了具体的剖析，在规格符合需求的前提下，能够发现程序与规格间的逻辑上的不符。可以在一定程度上保证程序的正确性。
测试则需要通过输入特定数据等方式，检查程序是否和预期相同，因为测试不可能穷举，导致了不穷举的测试不可能验证程序是完全正确的，只能验证程序在现有的测试情况下有没有发生错误。经过测试后的代码可能因为测试的不够全面仍然有错。尽管如此，测试依然是一种高效的检查程序的方法，通过输入数据或复现现场，直观的发现代码的问题，进而在代码中找到问题的来源并修正。
二、调研OCL语言，并比较其与课程所介绍的JSF规格之间的相似和不同之处
OCL语言的全称是Object Contraint Language，即对象约束语言，是UML中约束定义的语言。
这里有一个对OCL语言解释的比较具体的pdf。https://www.omg.org/spec/OCL/2.2/PDF
与JSF相比，两者的相似指出有：都可以描述不变量、前置条件、后置条件，都是基于数学中的谓词逻辑，有一个形式化的数学语义，理想情况下，都无二义性。
两者的不同之处有：OCL取了自然语言和数学符号的折中方案，使用普通的ASCII字符来表达数学中同样的概念，JSF强调使用数学语言。OCL是一个类型语言，任何表达式的值都是属于一个类型的。这个类型可以是预定义的标准类型例如Boolean或者Integer，也可以是UML图中的元素例如对象，也可以是这些元素组成的集合，例如对象的集合、包、有序集合等等。 但JSF中并没有对这一点做出要求。
三、根据第十四次作业的单电梯系统，针对调度器、电梯、请求队列和请求，至少整理出 一幅UML类图、一幅顺序图和一幅状态图，并使用图(graph)来表示出模型
类图
顺序图
状态图
四、整理总结一个学期所学所练
oo第一单元是基本的设计思想，介绍了java和对象，包括类的抽象，私有，接口和继承等等，是后续部分的奠基石。第二单元是多线程的数据管理和冲突解决，引入了多线程的编程方法。第三单元是规格化设计，为第四章论证铺垫。第四单元是单元测试和正确性论证，根据规格对每个方法进行测试和覆盖率检查，对每个类进行正确性论证。
多项式--->电梯调度--->文件监管--->出租车
在设计，测试和质量上有所进步。从不会写java程序到能写出来一个差不多面向对象的程序，收获很大。
积累了工程经验，虽然在课程中并没有亲自体验团队开发，但是在老师的引导下，也逐步理解了在工程中的规范以及合作，同时也理解了良好设计规格化设计的重要性，视野得到了延拓。