算法正确性

在 理论计算机科学 中, 当一个算法相对于一个规范来说是正确的时，它就被认为是正确的。功能的 正确性是指算法的输入输出行为(即，对于每一个输入，它产生预期的输出)。^[1]

在部分正确性(要求返回正确的答案)和全部正确性(另外还要求算法终止)之间进行了区分。由于对暂停问题没有一般的解决方案，因此完全正确性的确定可能要深入得多。终止性证明 是一种 数学证明 ，它在形式验证中起着至关重要的作用，因为算法的完全正确性取决于终止。^[2]

例如，连续搜索 整数 1，2，3，…看看我们是否能找到一些现象的例子，比如说一个奇数的完全数，很容易写出一个部分正确的程序（用长除法除以2来检查n是否完全）。但是说这个程序是完全正确的就等于确认了在数论中还不知道的东西。

假设算法和规范都是正式给出的，那么证明必须是数学证明。特别是，对于在给定机器上实现算法的给定程序来说，它不应该是一个正确的判定。这将涉及诸如计算机存储器限制之类的考虑 。

证明理论的一个深入的结果，即柯里-霍华德对应，声明构造逻辑中的函数正确性证明对应于 λ演算中的某个程序。以这种方式转换证明被称为程序提取。

霍尔逻辑 是一种特定的 形式系统 ，用于严格推理计算机程序的正确性。^[3] 它使用公理化技术来定义编程语言语义，并通过被称为霍尔三元组的判定来争论程序的正确性。

软件测试是旨在评估程序或系统的属性或能力并确定其满足所需结果的任何活动。尽管软件测试对软件质量至关重要，并且被程序员和测试人员广泛部署，但是由于对软件原理的理解有限，软件测试仍然是一门艺术。软件测试的困难源于软件的复杂性:我们不能完全测试一个中等复杂性的程序。测试不仅仅是调试。测试的目的可以是质量保证、验证和确认，或者可靠性评估。测试也可以作为通用的度量标准。正确性测试和可靠性测试是测试的两个主要领域。软件测试是预算、时间和质量之间的权衡。^[4]