测试和正确性论证分别是从理论和实践两个角度去规范程序的正确性的，我认为其主要的区别在于对于程序透明度的需求上，
测试作为一种实践手段，他的实施的要求是比较低的:在完全了解程序的结构下可以进行针对性的覆盖测试，在对程序一无所知的时候依旧可以进行压力测试和黑盒测试，但同样的，作为实践手段的测试无法从逻辑上完全的自洽，哪怕是覆盖性的测试，在论述其测试覆盖性的时候其实也经过了很多正确性论证的过程。简而言之，测试能为任何程序都提供一定限度的保证，但这个保障几乎不可能是完备的。
正确性论证是从理论原理和逻辑上证明程序的正确性和可行性，他相较于测试而言需要获得程序自身的全部信息，只有从逻辑层面到设计层面都通透的人才能对程序写出一份有效的正确性论证。其二，正确性论证往往也需要被测试所辅助，因为正确性论证本身的论证过程和实际实现过程都是可能出现人为的受迫性失误的。如果说测试是对程序现象的直接客观反映，在进行正确性论证的过程中的主观部分是很难以摒除的。概而论之，完成一份完美的正确性论证需要的是程序设计规程中的所有资源和细节，而且完美本身就是不可能达到的，但一旦完成了一份正确性论证，程序的逻辑正确性就被完备的保障了，无论程序以后再做何调整，这个单元是不会受到影响的。
测试的优点：
1.种类多样，开始测试的必要条件很少
2.针对性强，可以验证程序对某一类型的输入的处理能力
3.需求指向，可以模拟操作的实践情景
缺点：
1.缺乏逻辑和理论上的可靠性
2.难以获得完备的保障
3.针对性和覆盖性依旧需要正确性论证的部分内容进行辅助
正确性论证的优点：
1.一旦正确，便是逻辑上完全可靠的
2.通过逻辑耦合可以确保完备性
3.可以对每个独立的论证单元进行程序间迁移，在条件不变的情况下正确性也不变
缺点：
1.需要对程序整体逻辑结构和设计结构的高度理解
2.论证过程中可能出现非受迫性失误，需要测试辅助
3.实践性差，某个单元的论证错误很可能导致程序所有样例的崩溃
同：
二者都是形式化，声明，约束性语言，本质都是前置条件向后置条件的一个导向，对过程规格的关心程度有限。同时，二者都使用了数理化的逻辑，但是出于自然语言的转化困境，二者也都创立了一部分数理逻辑语言之外的，便于规范的新语法。
异：
OCL语言有JSF语言所没有的监控条件部分，使得作为一种约束语言的约束真值表达性更为强大，同时,OCL的语法结构相较于JSF更为复杂，这使得他更便于规格的书写，但难于对于规格的验证。
JSF语言比较于OCL语言多了Modifies域，更好的能够让书写者完成变量监控，同时JSF语言对布尔表达式的数理逻辑依赖性更强，这对书写者提升了抽象性的难度，但是在验证正确性和进行迁移的时候更为方便。
UML类图
UML系统时序图
UML状态图
四个单元是一个整体的学习流程，第一单元让我们熟悉面向对象的概念思想，第二单元完成线程协调，第三单元和第四单元则是测试和正确性论证，从整体的规划来说是先实践后理论，倒置了一个实际工程的实现流程让我们明白完成一个面向对象项目的四要素。
其实如果在默认同学们有一定的JAVA设计基础的话从第一单元就开始渗透一部分的规格思想会更好一些?毕竟补充规格的过程和设计规格的过程差异还是较大的，联系补充和调整可能并没能达到预期的教学目标
在这个学期的学习过程中，个人抽象问题的能力和面向对象设计类和方法的能力肯定是有所提升的，在最后几次对最初几次作业代码调整的过程中，都能够在保证正确性的前提下对代码进行大幅度优化。
这门课程是我第一次真正的接触单元测试，先前进行的都是黑盒和完全覆盖性测试比较多；Junit的功能不算强大，但是让我们初窥单元测试还是足够了。
着重考虑代码上的鲁棒性是这门课程给我最大的收获，现在在写代码之前，的确会比先前在代码的健壮性上考虑的全面更多。
一个规格，一个标准，工程化开发，流水化生产。易于分工，便与协作。高效，准确，可迁移。
课程两头松中间紧的情况太严重了，如果可能的话，能否从新平均分摊一下每一周的作业量和作业安排？
这届实施的错误分支树举措给予好评，的确真正有效的限制了乱报bug的情况，但是现在先挂满树再等人申诉坐地还钱的情况依旧是一本万利，希望课程组能够给被申诉的bug一个阈值，如果某一次作业测试者被申诉成功的bug点超过一定数目，要对测试者予以相应的惩罚。
最后，还是规格这里的教学方式问题，现在的课程安排的确很难让大家意识到他的重要性并去自发的好好学习，况且补充规格这件事的确对设计规格起到的帮助作用有限，是否可以从新考虑一下这里的作业和教学方式呢？哪怕是从规格设计起，用3次作业写一个新项目也是可以的啊
原文：https://www.cnblogs.com/eberwein/p/9217408.html