测试和正确性论证的效果差异
测试一般分为：功能测试、单元测试、鲁棒性测试、性能测试、回归测试等。测试的优点是操作简单粗暴；缺点是如果测试集不够大可能不能覆盖所有可能出现的场景，也就是说测试不够全面的问题。
正确性论证偏理论，是从逻辑层面分析代码正确性。其优点是能覆盖到代码的所有分支，从而保证代码的正确性；缺点是需要花费大量时间和精力。
OCL语言 VS JSF规格
OCL是一种形式语言，可以应用于任何实现方式的非正规语言，最初由IBM公司设计完成。虽然OCL是一种形式化语言，但是它具有形式化语言无二义性的特点，又消除了形式化语言的复杂性。传统意义上的形式语言一般仅适用于有一定数学背景的人，而没有相关知识培训的人则难以使用，也就是说传统意义上的形式语言对使用者要求较高，而OCL语言简练易上手，适用范围更广。
JSF规格约束没有OCL语言规范，尤其是用自然语言描述的JSF很容易造成歧义。
OCL和JSF的相似之处在于，OCL的前置条件用"pre"标识，后置条件用"post"标识，相当于JSF的"requires"和"effects"。且OCL和JSF都起约束作用。
OCL格式如下：
context Typename::operationName(param1 : Type1, ... ): ReturnType
pre : param1 > ...
post: result = ...
JSF格式如下：
/**
* @requires:
* @modifies:
* @effects:
* /
单电梯ALS调度
类图：
时序图：
状态图：
OO学期总结
作业清单：
第一次作业：多项式处理
第二次作业：傻子电梯
第三次作业：ALS电梯
第四次作业：多线程ALS电梯
第六次作业：文件系统
第七次作业：多线程出租车
第九次作业：多线程出租车+道路开闭
第十次作业：多线程出租车+红绿灯
第十一次作业： 多线程出租车+JSF+LSP原则
第十三次作业：单线程ALS电梯+JSF+Junit4覆盖性测试
第十四次作业：单线程ALS电梯+正确性论证
四个单元模块知识点：
1、熟悉面向对象编程方式和正则表达式的使用
2、多线程共享数据避免出现死锁问题，同步与互斥的处理
3、处理多线程时间错误的问题
4、JSF规范化、测试集全覆盖和正确性论证
设计、测试和质量上的进步：
OO这门课带给我很多，乌鸡老师在最后一节总结课上说的很对，上完面向对象这门课，我们的代码风格有了质的飞跃，主要体现在代码架构、编程技巧、规格编写等方面。
设计：从面向过程到面向对象，对象职责越来越明确，方法功能也逐渐清晰，代码也开始相对模块化。
测试：刚开始不知道怎么构造一个完备的测试集，像个无头苍蝇想到什么就写什么，经历了这个学期的互测，开始领悟到了测试的套路，擅于发现奇怪的边界情况。
质量：从方法长度可以明显感受到代码质量的变化，一个方法上百行到基本50行以内，方法功能也变得清晰明了，以及对象之间的交互信息也明确了不少。最重要的还有代码规范的问题，变量名和方法名等，刚开始我会取一个自己喜欢的或者有趣的名字比如“haha”“balabala”“bibi”之类的，回头看自己写过的代码时，读起来非常费劲，现在我已经成熟了，这些肤浅的命名绝不出现在我的代码中，对变量、方法命名的规范化使代码可读性大大提高！即使几周不看，还是很明确方法功能和变量的意义。
对工程开发的理解
我觉得工程开发需要一个团队合作来完成，通过git随时随地修改代码，对代码规范化要求高，提高团队合作效率。并且对测试要求也很高，听说测试不行的程序猿是要拿去祭天的QAQ
课程建议
issue上每次作业可以限制一下每个用户的提问次数，像这学期的电梯作业和出租车作业，助教得忙着看issue又要忙着回复各位同学的微信，心疼助教小姐姐们QAQ