正确性（计算机科学）

在理论计算机科学中，如果一个算法的行为符合规定，那么它对于一个规范来说就是正确的。探讨得xxx的是功能正确性，它指的是算法的输入-输出行为（即，对于每个输入，它产生一个满足规范的输出）。在后者的概念中，部分正确性，即要求如果返回的答案是正确的，与完全正确性是有区别的，后者还要求最终返回一个答案，即算法的终止。相应地，要证明一个程序的完全正确性，只需证明其部分正确性和终止。后一种证明（终止证明）永远不可能完全自动化，因为停止问题是不可判定的。例如，连续搜索整数1，2，3，......，看我们是否能找到某个现象的例子--比如说一个奇数完全数--写一个部分正确的程序是很容易的。但是说这个程序是完全正确的将是断言目前在数论中不知道的东西。证明必须是一个数学证明，假设算法和规范都是正式给出的。特别是，它不应该是一个在特定机器上实现算法的特定程序的正确性断言。这将涉及到对计算机内存的限制等考虑。证明理论中的一个深层结果，即Curry-Howard对应关系，指出构造逻辑中的功能正确性证明对应于λ微积分中的某个程序。以这种方式转换一个证明被称为程序提取。霍尔逻辑是一个特定的形式系统，用于严格推理计算机程序的正确性。

它使用公理技术来定义编程语言语义，并通过被称为Hoare三要素的断言来论证程序的正确性。软件测试是任何旨在评估程序或系统的属性或能力并确定其符合所需结果的活动。尽管对软件质量至关重要，并且被程序员和测试人员广泛部署，但由于对软件原理的理解有限，软件测试仍然是一门艺术。软件测试的困难源于软件的复杂性：我们不可能完全测试一个具有中等复杂度的程序。测试不仅仅是调试。测试的目的可以是质量保证，验证和确认，或可靠性估计。测试也可以作为一个通用指标。正确性测试和可靠性测试是测试的两个主要领域。软件测试是预算、时间和质量之间的权衡。