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

Question

我正在学习如何编程，但我无法理解的一件事是 preconditions 和postconditions。

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

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

Answer 1

它在这篇c++ 的论文中得到了很好的阐述

• 一个前提是应该持定的谓词进入的功能。它表达了函数对其参数和/或函数可能使用的对象状态的期望。

• 一个后置条件是，应当在举行谓词从退出的功能。它表达了条件，一个函数应确保为返回值和/或可以由函数中使用的对象的状态。

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

在 Dlang 中，基于契约的编程有很好的设计。本文档提供了一个示例：

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块中。

• 如果前置条件和后置条件都满足，那么它就会愉快地编译，就像传入9函数一样。live demo
• 如果不满足前提条件，就像传入-1函数一样。live demo

  core.exception.AssertError@prog.d(8): 断言失败

• 如果由于我们没有处理块中的逻辑而导致不满足后置条件do，例如 returnsquare而不是square-root，则后置条件将起作用：live demo

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

对于课堂，Dlang 也有不错的工具，阅读文档了解更多

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

这是提案，也许对理解它们也有帮助（不过，比 D 丑多了，恕我直言）

Answer 2

这是一个计算机科学问题，而不是一个编程问题，所以在https://cs.stackexchange.com/上更合适，但无论如何我都会回答它。

\n\n

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

\n\n

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

\n\n

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

\n\n

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

\n\n

（注：0 ..< i是指所有j这样的0 \xe2\x89\xa4 j < i。）

\n\n

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

\n\n

第二个后置条件断言大海捞针中不会出现在索引 i 之前的任何位置。因此，程序找到了第一根针（如果它找到了任何针）。

\n\n

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

\n\n

\xe2\x80\x9cprecondition\xe2\x80\x9d 是关于程序状态的断言，当与程序的后续操作结合时，可用于证明后置条件。我们可以在示例程序中添加前提条件：

\n\n

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

\n\n

（注：0 ... i表示所有j这样的0 \xe2\x89\xa4 j \xe2\x89\xa4 i。）

\n\n

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

\n\n

您可以使用归纳法来证明每次程序到达前提条件时都为真。当条件为假时循环结束，这意味着第一个后置条件为真。（第一个后置条件是循环条件的逆命题。）循环前置条件为真意味着第二个后置条件也为真。

\n