一、论述测试与正确性论证的差异
我认为论述测试代表从理论的角度来进行运行正确性的判断，而正确性测试则是从实践的角度来看待程序的正确性问题。两者之间有着明显的差异。
正确性论证是仅仅从代码的逻辑结构方面来分析代码实现的正确性，这需要测试者对于被测试程序结构以及其要实现的功能的充分了解，这对于一个素昧平生的测试者来说可能是很难的。但是从另一方面来说，如果测试通过就能保证程序在逻辑方面是完全可靠的。
而论述测试更多的是从实际出发，有对整体功能实现的测试，也可以对单个方法测试，这种方法有相当大的灵活性，但是却不能保证代码实现的正确性。
二、JSF与OCL异同
两者都是采用前置条件与后置条件，对于方法实现的过程不给予太多的关注。同时两者都是要求前置后置条件的描述必须使用数理化逻辑，这也出现了许多数理化逻辑难以描述的困难。
不同的是JSF还要求对于modified的描述，便于更好的对方法内部改变的成员变量的监控。
三、
状态图：
类图：
顺序图：
四、总结
这个学期在我看来是非常充实的，OO这门课程让我学会了很多东西，首先java这门编程语言的使用自然是不用多说，最重要的是面向对象思想，以及如何将这种思想体现在自己的代码上，回顾自己第一次的代码，确实还是没有摆脱大一时候的面向过程编程思想，虽说也分了几个类，大不过是敷衍了事，并没有理解其中的奥秘，就好像一个裸身，没有任何的修饰。随着课程的深入，线程并发执行，程序的规格，正确性论证等等，也是为了能让我们养成良好的编程习惯，减少程序的错误，自己的程序也开始渐渐换上了衣裳，成员变量的保护，方法的缩减，逻辑的清晰，虽然还远远未及工程上的要求，但是不管怎么说还是有很大的进步，从一开始连java都不会，慢慢会写规格了，真开心！？
课程的安排还是很合理的，第一单元讲设计，设计是一个程序实现的基础，良好的设计是后面所有过程能够完成执行的基础，第二单元开始线程并发，这几次作业难度还是很大的，不仅是类里面的良好设计，同样重要的是线程之间同步与互斥，做好了同步才能保证对于共享区域的读写不会出现问题。再到后面的规格，正确性论证，都是为了规范化我们的代码，为了能让他人更好的理解我们的代码。
所谓工程化开发，我认为是一种在实际开发中经常用到方式，工程化开发有几个很明显的特点，包括代码的可读性，可延展性等等，这些都是为代码的合作做准备，因为工程化开发不可能所有的事情都由一个人来完成，所以当一个人在编写程序的时候，不仅仅只需要考虑自己代码的功能完整性，还需要考虑自己的代码的可读性，对其他程序员是否友好，合作与发展是当今社会的主题，这同样也体现在了工程化开发之中。
对于课程组的建议就是是否能够将课业负担分配的都平均点，就是希望每次作业都像多线程电梯那么难，的工作量平均分配，对于前几个班他们周三要上课，碰巧前部分的作业更难，所以经常熬夜，对身体不好。