6

私はプログラミングの方法を学んでいますが、頭を悩ませることができないのは、 preconditions とpostconditionsです。

関数を呼び出す前の if ステートメントは前提条件と見なされますか、それともほとんどの言語でこれを行う別のより効率的な方法はありますか?

また、プログラミングに関する現在の知識で理解できる前提条件の例を見つけるのに苦労しています。誰かが単純なものを証明できれば、本当に感謝します（どの言語でも問題ありません）

4

3 に答える 3

4

これはコンピューター サイエンスの質問であり、プログラミングの質問ではないため、 https://cs.stackexchange.com/の方が適切ですが、とにかく回答します。

干し草の山から針の最初のインデックスを見つけるこのプログラムを考えてみましょう。(干し草の山にはたくさんの針が含まれている可能性があります。最初の 1 つで止めたいと思います。) 干し草の山に針が含まれていない場合、インデックスは干し草の山のサイズと等しくなります (干し草の山への有効なインデックスではありません)。

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すべてを意味します。)j0 ≤ j < i

最初の事後条件は、i が干し草の山にあるアイテムの数、または i が針のインデックスであることを表明します。

2 番目の事後条件は、インデックス 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すべてを意味します。)j0 ≤ j ≤ i

前提条件は、 index の要素までのすべての干し草の山要素iが針ではないことを示しています。

帰納法を使用して、プログラムが前提条件に到達するたびに前提条件が真であることを証明できます。条件が false の場合、ループは終了します。これは、最初の事後条件が true であることを意味します。(最初の事後条件はループ条件の対比です。) ループの事前条件が真であったという事実は、2 番目の事後条件も真であることを意味します。

于 2016-02-09T23:17:46.473 に答える