一、程序测试是指测试者特意挑出一批输入数据，通过运行程序，检查每个输入数据所对应的运行结果是否符合预期要求。
正确性证明是论证程序达到预期目的的一般性陈述，而该论证与程序输入数据的特定值无关，能够代表穷举性测试。
而Dijkstra说过“程序测试只能证明程序有错，不能说明程序正确”。除非进行穷举行测试。因为就单独一个测试用例而言，不能肯定程序在这个用例的方面没有出错。而且，穷举性测试对于大型程序而言，一是比较难以实现，二是这样测试费时费力，得不偿失。而正确性论证则是从逻辑推理的方面，论证程序可能的输入对应相应的输出，不需要穷举，也不需要特定的用例。这种方法的缺点是论证一定要严密，而且要考虑所有的情况。所以，在实际的测试中，通常会两者结合使用。
二、OCL(object constraint language) 对象约束语言。用来进行约束定义的，形式化的无二义的语言。OCL于1995年由Warmer等人，在IBM设计成功，并开始使用。1997年UML的1.1版本正式采用OCL。, OCL作为图形符号的补充，说明建模元素的有关细节，例如：约束，前置条件，后置条件等。
OCL原则主要有：声明性语言，不会改变模型中的内容；形式化语言语言无二义规范语言；类型性语言，每一个表达式都有类型；易学好用。
OCL作为形式化语言,基本语言要素包括:类型(基本类型，高级类型)、操作、表达式、语句。OCL的基本类型包括整型,实型,字符串型,布尔型。OCL定义的高级数据类型有群,集合,袋和序列.其中群是抽象数据类型,集合,袋和序列是群的子集。
接下来有几个OCL的例子：
1.
context Person inv:
Person.allInstances->forAll(p1,p2|
p1<>p2 implies p1.name <> p2.name)
对类Person的所有对象实例,要求它们的名字必须唯一
2.
context Person inv:
let income = self.jobsalary->sum() in
if isUnemployed then
income < 100
else
income >= 100
endif
对类Person的收入是工作薪水求和,但有限定条件.
OCL与JSF都是一种约束语言，都是为了帮助别人更好的理解我们所写的程序，他们都有前置条件，后置条件，都可以用来约束操作。但是OCL应用更为全面，OCL表达式的上下文表示这个表达式所作用的范围，可以是类，类的属性和操作。而JSF不能做到，而且OCL的语言更加规范，每一种数据类型都有自己的操作方法，OCL的语言更容易理解，保留了很多自然语言的写法。JSF是相对来说构造起来简单，但是描述并不简单，稍显复杂。
三、第十四次作业整理的UML类图，顺序图，状态图如下。
类图：
顺序图：
状态图：
四、
1.本学期我们一共有四个模块，第一个模块主要是让我们熟悉java环境，写一些简单的程序；到第二个模块，就增加了多线程编程，初次接触还是挺难的；其次是工程化开发，对于多线程编程提出了更高的要求，也有了更多的感悟；最后是测试自己的程序并编写规格，这是为了让我们更加领悟工程化方法的精髓。
2.对于自己而言，本学期还是有很多收获的。本来自己对java没有一点基础，也没有接触过，所以开始的代码写的很差劲，明显是面向过程式的编程，但后来随着课程的深入，自己也对java开发有了更深的理解，到后面几次作业，bug明显就少很多了，自己不仅在代码质量上有了进步，更主要是设计思想有了变化，我觉得这是很关键的，知道从总体去构造一个程序，而不是盲目的去瞎写。
3我认为工程化开发吧，就是从系统或者更高的层面来看待一个程序吧，高屋建瓴大概就是这种感觉。一个工程，相对来说，是一个比较大的对象，万丈高楼平地起，得从底层就为它打好基础，使用更规范的写法，命名，以及编写测试用例，方法更加简洁，单一等等，我觉得这都是本学期OO带给我的工程化的感悟吧
4.最后，祝OO越办越好。