一、测试与正确性论证
程序的测试分为大小不同的几个阶段，我们在这个阶段的作业中进行的是基于JUnit测试框架的单元测试。
单元测试是指对程序中最小的可测试单元进行测试。我们测试的单元是方法。单元测试的特点使是从结果出发，寻找代码的漏洞。一个全面的单元测试能够对覆盖到方法执行过程中遇到的所有情况，也就是覆盖所有分支条件。通过单元测试则说明该方法能够完全符合期望的规格。因此，单元测试的优点是能够确保一个方法的正确性。然而构造一个完美覆盖的单元测试很难，尤其是当原方法的分支条件很多的时候。编写单元测试通常要花费比编写原方法更多的时间。
正确性论证也是证明方法是否符合期望规格的手段。与单元测试从结果出发不同，正确性论证是从代码逻辑出发，论证方法如何完成规格。正确性论证更像是数学中的证明题，需要严谨严密的逻辑思维。完成正确性论证的前提是对代码逻辑完全掌握。
正确性论证能够对所有分支进行论证，较单元测试来说更容易达到完全覆盖，然而正确性论证过程较为复杂，相比单元测试"粗暴"地判断对错来说更难保证论证结果的正确性。
由于二者具有各有优劣，可以互相补充，二者兼用能够更充分的保证代码的正确性。
二、OCL语言
OCL(object constraint language)语言即对象约束语言。它是一种用于约束指定模型的定义，形式化的没有二义性的语言。
OCL拥有自己的语法体系，有数据类型和运算符，更优高级数据类型例如群、集合、袋和序列。在对象约束方面，OCL表达式包括不变量、前置条件和后置条件等。
OCL同我们学习的JSF用途相同，都是用于描述对象的约束规范的形式化语言。用二者描述的约束都是没有二义性的。不同的是，OCL有一套比JSF更加完备高级的语法结构，而JSF只有二阶逻辑结构，没有高级的分支语句等，也没有对数据类型的描述。
三、单电梯系统模型
UML类图：
UML顺序图：
UML状态图：
四、学期总结
知识点梳理
课程分为四个模块。
第一个模块主要熟悉面向对象编程方法以及对象机制。这个模块是对java语言和面向对象的初步接触。
第二个模块是多线程编程，以及线程安全问题。这个模块训练了多线程的思维。
第三个模块是规格设计。这个模块我们将代码规范化，使代码更加规格化、模块化。
第四个模块是基于规格的测试与论证。这个模块学习了更加严谨规范的测试方式。
可以说这四个模块之间就是四层积木的关系，层层递进，让我们从零开始体会面向对象程序从构思、实现到测试的完整过程，并在这个过程中逐渐强化面向对象的编程思想。
进步总结
在此之前完全没有接触过面向对象有关知识，编程还停留在一个程序几个方法的过程式编程中。在第一次多项式的编程中，我仅仅使用了两个对象，且没有做到对象的封装，这两个对象之间相互调用，逻辑十分混乱；第三次ALS电梯在重构之前更是在调度类中一个方法写了两百多行，完全没有做到方法的抽象，导致程序十分臃肿，很多BUG发现了却无法定位修复；
从多线程电梯开始决定优化代码结构，至此开始，以后的作业中慢慢形成了面向对象的基本思想和思路框架，代码结构也在一次次训练中得到改善。
总的来说进步非常明显。通过这门课程的高强度训练，现在能够比较完整的从问题中抽象出对象并进行模块化的编程，代码的规范程度也有很大提高。但仍有很多不足之处，例如对接口的理解感觉不是很深刻。
对工程化开发理解
工程化即系统化、模块化、规范化的过程。指将具有一定规模数量的单个系统或功能部件，按照一定的规范，组合成一个模块鲜明、系统性强的整体。工程化开发的关键是封装，将各种资源封装成一个个模块之后，我们不必再关心该封装下的具体细节，只需要将这些模块组装成一个整体就能够形成一个完整的工程。
面向对象的设计原则与工程化开发中模块化的要求不谋而合，然而面向对象设计缺乏清晰的层次关系，面对复杂的操作过程时实现效果不佳，涉及多个对象之间共同协作时也会显得不那么灵活，这是面相对象设计的一个不足之处。
规格设计是工程化开发最重要的一环。良好的规格约束能够便于团队合作与相互理解，实现更好的协作关系。
对课程的期望与建议
- 尽可能在最初介绍更多的关于java语言的知识，或者哪怕提供更多资料也可以。
- 希望能够有更多更完整的程序实例和讲解，现有的ppt上的例子对于作业来说完全不是一个层次上的，导致我们拿到作业的时候感觉难度的跳跃很大。特别是多线程部分，我想多一点复杂的多线程程序例子对于我们理解多线程操作来说更有帮助。
- 关于互测部分，特别是规格互测的时候，恶意乱报规格BUG的现象比较严重，我认为在报告规格BUG部分的机制欠妥。
- 还是互测，我提出一个关于issue的问题。对于指导书没有规定的内容，很多完全可以自行定义而不影响整个程序的正确性的问题，由于助教一句话我们就只能根据助教的理解方式修改程序。有时候这种修改需要花费很多精力，甚至更改整个代码的结构；甚至有一次由于助教理解错误造成我改过去又改了回来。。。我认为这些边角部分的问题不影响教学核心，可以给予我们充分的自由。否则这些东西会在无形之中增加我们的负担，本身课下任务量就很大，这些原本很小的问题可能会打击对课程的热情和积极性。