文档介绍：程序正确性证明
主要内容
程序正确性简介
程序测试
程序正确性证明
内容线索
程序正确性简介
程序测试
程序正确性证明
程序的正确性
所谓一段程序是正确的,是指这段程序能准确无误地完成编写者所期望赋予它的功能。
或者说,对任何一组允许的输入信息,程序执行后能得到一组和这组输入信息相对应的正确的输出信息。
通俗地说,“做了它该做的事,没有做它不该做的事”
程序正确性的严格定义分为三种类型
部分正确性
终止性
完全正确性
如何保证程序的正确性
要求
1、从编程时就应该尽量地避免和减少错误的发生
2、当程序编好后要尽量找出错误,纠正错误
避免错误的方法
1、程序的结构要简单
2、采用标准的软件设计工具、标准的算法手册以及有效的程序设计方法
发现错误的方法
1、利用测试工具
2、利用程序的验证系统
程序测试
测试是程序的执行过程,目的在于发现错误。
一个好的测试用例在于能发现至今未发现的错误;
一个成功的测试是发现了至今未发现的错误的测试。
测试的原则
1. 应当“尽早地和不断地进行软件测试”。
2. 测试用例应由测试输入数据和对应的预期输出结果组成。
3. 程序员应避免检查自己的程序。
4. 在设计测试用例时,应当包括合理的输入条件和不合理的输入条件。
5. 充分注意测试中的群集现象。即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比。
6. 严格执行测试计划,排除测试的随意性。
7. 应当对每一个测试结果做全面检查。
8. 妥善保存测试计划,测试用例,出错统计和最终分析报告,为维护提供方便。
内容线索
程序正确性简介
程序测试
程序正确性证明
简介
Floyd不变式断言法
Hoare规则公理方法
Dijkstra最弱前置条件方法
正确性证明
测试只能发现程序错误,但不能证明程序无错。即所谓“挂一漏万”。
原因:测试并没有也不可能包含所有数据,只是选择了一些具有代表性的数据,所以它具有局限性。
正确性证明是通过数学技术来确定软件是否正确,也就是说,是否符合其规格说明。
正确性证明的发展