一、测试与正确性论证
测试与正确性论证是从系统的不同层面对其可靠性进行验证。
正确性论证能够从类的规格以及方法过程规格出发，对代码实现进行逻辑上的证明，更加稳定可靠，正确性论证的难点在于，并不是系统的每个部分都可以很轻易的使用数学语言建模，在很多情况下不易论证。正确性论证在操作上有一定的难度。
测试更偏重于模拟应用场景，通过欧运行大量的测试用例来覆盖运行代码的每个分支从而对程序整体进行正确性检验，不过相对于正确性论证，缺乏严谨性，不能像正确性论证一样可以全面的论证程序的正确性。
二、OCL语言
对象约束语言(Object Consttraint Language, OCL)是用来进行约束定义的，形式化的无二义语言。它是声明性语言，不会改变模型中的内容，是一种类型性语言，每一个表达式都有类型，易学好用。
它与JSF的相似之处：
1.都可以描述不变量、前置条件和后置条件；
2.都是基于数学的为此逻辑，有一个形式化的数学语义；
3.无二异性。
与JSF的不同之处：
1.OCL使用ASCII字符表达数学中的概念，而JSF强调使用数学语言；
2.OCL是一种类型语言，任何表达式的值都属于同一类型，但JSF在这一方面并没有要求。
三、图
1.UML类图
四、学期总结
1.知识点关系梳理
2.程序梳理
3.对工程化开发的理解
工程化开发需要遵循一些特定的规则，不仅方便自己审查代码，也方便代码的交流理解，毕竟程序有不确定性且代码规模日益增大，所以需要提高开发效率，降低维护难度，这是必行之举。
4.对课程的期望与建议
1.建议老师及助教将指导书中不够明晰的地方统一一下，可以减少同学在码代码时浪费在研究要求上的时间；
2.衷心希望老师们不要把熬夜当成什么光荣的事情，并对此加以支持和鼓励。就我了解，有部分同学经过熬夜已经相当不适，虽说学习进步是喜闻乐见的事，但身体应该是更为重要的基础吧。