什么是前置条件和后置条件？答案

【问题标题】：What are preconditions and postconditions?什么是前置条件和后置条件？
【发布时间】：2016-02-09 22:20:43
【问题描述】：

我正在学习如何编程，但我无法完全理解的一件事是前置条件和后置条件。

调用函数之前的 if 语句是否被视为前提条件，或者在大多数语言中是否有单独的更有效的方法？

我也在努力寻找任何 先决条件的例子，如果有人能证明一个简单的例子，我可以理解我目前的编程知识，那么我将非常感激（任何语言都可以)

【问题讨论】：

标签： programming-languages design-by-contract preconditions post-conditions

【解决方案1】：

这个c++'s paper里说得很清楚

前置条件是一个谓词，它应该在进入函数时保持不变。它在其参数和/或该函数可能使用的对象的状态上表达了函数的期望。

后置条件是一个谓词，应该在退出函数时保持不变。它表达了函数应确保返回值和/或函数可能使用的对象的状态的条件。

前置条件和后置条件属于基于契约的编程。

在 Dlang 中，基于契约的编程有很好的设计。 This document提供样品：

long square_root(long x)
in
{
    assert(x >= 0);
}
out (result)
{
    assert(result ^^ 2 <= x && (result + 1) ^^ 2 > x);
}
do
{
    return cast(long)std.math.sqrt(cast(real)x);
}

前置条件在in块中，后置条件在out块中。

如果 preconditions 和 postconditions 都满足，那么它将顺利编译，就像将9 传递给函数一样。 live demo
如果不满足先决条件，例如将-1 传递给函数。 live demo

core.exception.AssertError@prog.d(8)：断言失败
如果后置条件不满足，这可能是因为我们没有处理do块中的逻辑，比如返回square而不是square-root，那么，后置条件将起作用：live demo

core.exception.AssertError@prog.d(13)：断言失败

对于课堂，Dlang 也有很好的工具，阅读the document 了解更多

顺便说一句，c++ 还将合约设计列入 c++20 的草案：https://www.reddit.com/r/cpp/comments/8prqzm/2018_rapperswil_iso_c_committee_trip_report/

Here 是建议，也许对理解它们也有帮助（虽然，比 D 丑得多，恕我直言）

【讨论】：

【解决方案2】：

这是一个计算机科学问题，不是编程问题，所以https://cs.stackexchange.com/ 更合适，但我还是会回答。

考虑这个程序来寻找大海捞针的第一个索引。（干草堆可能包含许多针；我们想停在第一个。）如果干草堆不包含针，则索引等于干草堆的大小（这不是干草堆的有效索引）。

i = 0
while i < haystack.count && haystack[i] != needle {
    i = i + 1
}

“后置条件”是关于程序状态的断言，通常表示程序已经计算了一些有用的东西（在后置条件点）。对于示例程序，我们可以编写后置条件断言它计算了我们想要的结果：

i = 0
while i < haystack.count && haystack[i] != needle {
    i = i + 1
}
assert(i == haystack.count || haystack[i] == needle) // first postcondition
haystack[0 ..< i].forEach { assert($0 != needle) } // second postcondition

（注意：0 ..< i 表示所有j 使得0 ≤ j < i。）

第一个后置条件断言 i 是大海捞针的数量，或者 i 是针的索引。

第二个后置条件断言在索引 i 之前的任何地方都没有出现在大海捞针中。因此程序找到第一根针，如果它找到任何针。

因此，如果这些后置条件为真，程序就会执行我们想要的操作。

“前置条件”是关于程序状态的断言，当与程序的后续动作结合时，可用于证明后置条件。我们可以在示例程序中添加前置条件：

i = 0
while i < haystack.count && haystack[i] != needle {
    haystack[0 ... i].forEach { assert($0 != needle) } // precondition
    i = i + 1
}
assert(i == haystack.count || haystack[i] == needle) // first postcondition
haystack[0 ..< i].forEach { assert($0 != needle) } // second postcondition

（注意：0 ... i 表示所有j 使得0 ≤ j ≤ i。）

前提条件告诉我们，直到并包括索引i 处的元素在内的所有干草堆元素都不是针。

你可以用induction来证明每次程序到达前提条件都是真的。循环在其条件为假时结束，这意味着第一个后置条件为真。（第一个后置条件是循环条件的反例。）循环前置条件为真意味着第二个后置条件也为真。

【讨论】：

【解决方案3】：

这是对这个人进行数学运算的错误方法。首先，变量并不全部存在，并且由于缺少变量的简单事实，解决方案循环不正确。此外，由于上述缺失变量和实际方程中的不稳定性，如果没有双盲研究和 1 个绝对变量，您将无法获得该方程的解。这随后使您的方程式开始无效。最后，由于我碰巧是一个挥舞着魔法的半智能聪明驴，我可以争辩说，如果一个人希望在大海捞针中找到一根针，那么只需点燃一根火柴并等待。当所说的干草堆消失时，请使用磁铁。问题没有数学解决。

【讨论】：