一.测试与正确性论证
测试与正确性论证是从系统的不同层面对其可靠性进行验证。
正确性论证更加稳定可靠，在软件系统的设计中有形式论证(Formal Verification)，即据某个或某些形式规范或属性，使用数学的方法证明其正确性或非正确性。正确性论证的难点在于，并不是系统的每个部分都可以很轻易得使用数学语言建模，即便是在我们的课程中使用的基于规格进行正确性论证，已经做了简化，但是仍有很多情况下不易论证。从对一个并不十分复杂的电梯控制系统进行规格论证就需要上万字来看，正确性论证在操作上有一定的难度。
而测试则更偏重于模拟应用场景，用样例将bug命中。当然测试也并非不具备复杂性，经过尝试使用Junit之后，我发现即便是构造测试用例也可以形成一个庞大的理论体系。
正确性论证和测试各有优劣，在实际应用中可以根据程序的规模、测试的可行性以及对可靠性的要求程度等情况，合理选择验证方式。适合的才是最好的。
二.OCL语言
OCL是一种描述UML建模细节的对象约束语言，它是UML标准的一部分。OCL是一种声明式语言，大部分表达式执行后会返回一个布尔值 。关于它的基本内容，Wikipedia描述如下：
OCL is a descendant of Syntropy, a second-generation object-oriented analysis and design method. The OCL 1.4 definition specified a constraint language. In OCL 2.0, the definition has been extended to include general object query language definitions.
OCL statements are constructed in four parts:
- a context that defines the limited situation in which the statement is valid
- a property that represents some characteristics of the context (e.g., if the context is a class, a property might be an attribute)
- an operation (e.g., arithmetic, set-oriented) that manipulates or qualifies a property, and
- keywords (e.g., if, then, else, and, or, not, implies) that are used to specify conditional expressions.
与JSF相比，两者的相似指出有：
- 都可以描述不变量、前置条件、后置条件
- 都是基于数学中的谓词逻辑，有一个形式化的数学语义
- 理想情况下，都无二义性
两者的不同之处有：
-
OCL取了自然语言和数学符号的折中方案，使用普通的ASCII字符来表达数学中同样的概念。 例如一个简单的OCL实例为：
context Person::getsChild() post: self.childs->notEmpty() and self.childs->size() > self.childs@pre->size()JSF强调使用数学语言
-
OCL是一个类型语言，任何表达式的值都是属于一个类型的。这个类型可以是预定义的标准类型例如Boolean或者Integer，也可以是UML图中的元素例如对象，也可以是这些元素组成的集合，例如对象的集合、包、有序集合等等。 但JSF中并没有对这一点做出要求。
三.UML
- UML类图
- UML序列图
- UML状态图
四.总结体会
1.知识点联系
2.成果
3.收获
-
这学期的很多东西都是从0开始学的：Java，Markdown,正则表达式，爬虫……
-
学会使用面向对象思想设计程序，从最初的只能勉强强行拆出四五个类到最后设计时不新建一个类会感到很不舒服，慢慢地适应了面向对象这种新的思维方式。
-
熟悉了多线程编程，并发式设计是我之前从未体验过的，同时自己亲自体会了线程的同步控制，也对操作系统中的进程并发有了更深刻的认识。
-
积累了工程经验，虽然在课程中并没有亲自体验团队开发，但是在老师的引导下，也逐步理解了在工程中的规范以及合作，同时也理解了良好设计的重要性。视野得到了延拓，看代码的视角从简单的语法层面到了需求、设计、维护等更广阔的层面。
-
锻炼了抗压能力，每周从周五晚上开始到下一周周五上午结束是一个循环，这个学期就是在一轮一轮循环中度过的，在整个循环的不同阶段，情绪会受到不同外界因素的影响，例如ddl导致的焦虑、树上莫名挂满bug的愤懑、对需求的不解，有时会微微失控，但是经过自我调节还是可以回归平稳，对自我情绪的把控力提高也是一项进步。
