一.正确与测试性论证

　　测试使用特定数据对我们的功能进行针对性测试，好处在于可以很直观很明显的找到bug所在，并且复现性也很强。他的实施的要求是比较低的:在完全了解程序的结构下可以进行针对性的覆盖测试，但是偏向于穷举，也就是我们平常对于自己的数据集过小，而担心自己有没有完全覆盖所有的可能，这种方式便于实现与分析，但是不能完全验证程序正确性。

　　正确性论证，就是通过分析需求，撰写规格后，论证程序符合规格的过程，偏向于验证程序的思路走向，逻辑判断等问题。正确性论证需要深入代码，他要获得程序自身的全部信息。正确性论证几乎可以做到全覆盖，涉及到了所有的情况。由于判断多为布尔型语言等，编写过程和阅读会比较费时间，但是验证上非常简单。

　　测试倾向于论证具体情况，正确性论证倾向于论证整体全部情况。

　　就我个人而言，主要还是测试为主，正确性论证为辅。在实际应用中根据实际情况，合理选择验证方式

 

二.OCL与JSF

　　对象约束语言简称OCL（Object Constraint Language），它是一种用于施加在指定的模型元素上约束的语言。OCL表达式以附加在模型元素上的条件和限制来表现对该对象的约束，其中包括附加在模型元素上的不变量或约束的表达式，附加在操作和方法上的前置条件和后置条件等。

　　对象约束语言是一种形式化语言，它主要用于表示UML模型中施加于模型上的约束。OCL具有如下特点：

    1、OCL是一种精确的，无二义性的语言

    2、OCL是一种规范说明性语言，所有有关实现的问题都不能用OCL来表达

    3、OCL是一种纯表达式语言，它是具有没有任何副作用的申明性语言。

    4、OCL是一种类型化语言，即OCL中的每一个表达式都是具有类型的。

    5、OCL不是一种程序设计语言，不能用OCL编写程序逻辑和控制流程。

　　相同点：

　　　　都是形式化的约束语言，在程序中进行无二义的逻辑约束。结构上也具有相似性，OCL主要包括的不变量，前置条件，后置条件，监护规则分别对应JSF对应着

　　　　repOK()，REQUIRES，EFFECTS和MODIFIES。

　　不同点：

　　　　他们的不同点在于作用的时间不同，OCL主要是在编写程序前，理论建模时刻对每个类进行明确的约束，而JSF主要在功能实现前进行约束以确保程序逻辑实现正确。

三.UML

 

时序图：

 

 

 

 

状态图：

 

 

 四.学期总结

　　四个单元： 　　

　　首先从多项式计算到傻瓜电梯，熟悉面向对象的概念思想。然后扩展电梯功能，引入了多线程。这一部分除了线程的操作外，还有线程的安全。除了完成规定的任务还要考虑数据的安全。之后引入规格化设计，在程序功能逐渐完善同时，也要考虑到我们的代码能否被他人看懂，能否便于移植，所以我们更要考虑程序实现中规格的规范，通过前置条件，后置条件对调用方法进行规范，对正确性进行统一的验证。最后引入了很多自动化测试，在代码规模提升后引入程序来进行自动化的覆盖全面的试，抽象全面的论证程序的正确性。

　　进步：

　　　　对面向对象思想有所掌握以及对一些规格和正确性论证有了初次的学习。

　　对工程化开发的理解

　　　　因为代码量比较多，工作量也比较大，不能在无脑写，应该先设计好代码的规格，然后通过写代码完成规格的实现

　　对课程的建议

　　　　希望面向对象课程能变得越来越好，而不是让越来越多的人去讨厌