什麼是先決條件和後置條件？

Question

我正在學習如何編程，但有一件事情我無法完全理解是先決條件和後置條件。

在調用被視爲前提條件的函數之前，if語句是否存在，或者在大多數語言中是否有單獨的更有效的方法？

我也苦苦尋找，我可以用我目前的編程知識瞭解的先決條件中的任何例子，如果有人能證明一個簡單的話，我會很感激它（任何語言將被罰款）

Answer 1

這是一個計算機科學問題，而不是一個編程問題，所以在https://cs.stackexchange.com/上更合適，但我會回答它。

想想這個程序，找到大海撈針中的第一個索引。 （草垛可能包含許多針，我們想停在第一個針上。）如果草垛不包含針，那麼指數就等於草垛的大小（這不是乾草堆的有效索引）。

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

A「後置條件」是關於一個程序，通常說，該程序已經計算的東西（在後置條件的點）有用的狀態的斷言。對於示例程序，我們可以寫後置條件斷言它計算我們想要的結果：

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 = 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來證明每次程序到達時前提條件都是正確的。當條件爲假時，循環結束，這意味着第一個後置條件爲真。 （第一個後置條件是循環條件的對立。）循環前提條件爲真的事實意味着第二條件條件也是成立的。