程序正确性是指 程序在指定的前提下，能够执行预定的行为并达到预期的结果。具体来说，程序正确性可以细分为以下几种类型：
部分正确性：
程序至少执行了某些预期的行为，但没有执行所有可能的行为。部分正确性通常通过霍尔三元组（Hoare triples）来表示，形式为 { P } c { Q }，其中 P 和 Q 是一阶逻辑的断言，c 是一个程序。
终止性：
程序在有限的步骤后能够停止，并且停止时满足某些条件。这意味着程序不会陷入无限循环或无限递归。
完全正确性：
程序不仅终止，而且返回一个正确的结果，并且对于所有可能的输入，都能产生正确的输出。
程序正确性的证明通常采用数学方法和逻辑推理，以确保程序在各种情况下都能按照设计者的意图正确执行。这包括使用归纳断言法、不变式断言法、子目标断言法等。
总结来说，程序正确性是软件质量的关键指标，它要求程序在规定的条件下能够可靠地执行预期的功能，并且没有错误或缺陷。通过严格的证明和测试，可以确保程序的正确性，从而提高软件的质量和可靠性。