6

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

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

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

4

3 回答 3

6

在这篇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 丑得多，恕我直言）

于 2018-06-09T12:25:58.057 回答
4

这是一个计算机科学问题，而不是编程问题，因此在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都不是针。

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

于 2016-02-09T23:17:46.473 回答
0

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

于 2021-10-09T04:32:17.430 回答