proof - 形式論理の正しさの証明

Question

誰かがこの質問に答えるのを手伝ってくれるかどうか疑問に思っていました. これは以前の試験用紙からのものであり、今年の試験の準備ができている答えを知っていればできることです。

この質問は非常に単純に思えて、完全に道に迷ってしまいます。正確には何を求めているのでしょうか?

整数変数を含むコードの次のセクションを検討してください。
if (i < j) {
    m = i;
} else {
    m = j;
}
適切な出力条件を記述し、コード片の正確性を検証することにより、実行後に m が i と j の最小値に等しいことを証明します。

私は投稿条件を次のように持っています: {m = i ∧ i < j ∨ m = j ∧ j < i}

これは正しいです？そして、これをどのように確認しますか？

score 2 · Accepted Answer

あなたの投稿条件は正しいです。個人的には、次のバリアント (同等) の方がより自然だと思います。

(i<j → m=i) ∧ (i≥j → m=j)

プログラムが事後条件を満たしていることを証明するには、次のようにします。

プログラムが常に事後条件を満たしていることを確認するtrueには、事前条件として使用する必要があることに注意してください。

したがって、次の Hoare トリプルがあります。

{true}
if (i < j) {


    m = i;

} else {


    m = j;

}
{(i < j → m = i) ∧ (i ≥ j → m = j)}

事後条件は両方のブランチの最後で保持する必要があるため、(条件の標準的な最も弱い前提条件ルールに従って)次のようになります。

{true}
if (i < j) {


    m = i;
    {(i < j → m = i) ∧ (i ≥ j → m = j)}     <--.
} else {                                       |
                                               |
                                               |
    m = j;                                     |   copy
    {(i < j → m = i) ∧ (i ≥ j → m = j)}     <--|
}                                              |
{(i < j → m = i) ∧ (i ≥ j → m = j)}  ----------'

割り当て利回りの最も弱い前提条件に従って式をさらに押し上げる

{true}
if (i < j) {

    {(i < j → i = i) ∧ (i ≥ j → i = j)}   <---.
    m = i;                                    | m replaced by i
    {(i < j → m = i) ∧ (i ≥ j → m = j)}   ----'
} else {

    {(i < j → j = i) ∧ (i ≥ j → j = j)}   <---.
    m = j;                                    | m replaced by j
    {(i < j → m = i) ∧ (i ≥ j → m = j)}   ----'
}
{(i < j → m = i) ∧ (i ≥ j → m = j)}

true ブランチi < jの上部では、else ブランチの上部では次のことがわかってい¬(i < j)ます。

{true}
if (i < j) {
    {i < j}                               (1)  <--- added
    {(i < j → i = i) ∧ (i ≥ j → i = j)}   (2)
    m = i;
    {(i < j → m = i) ∧ (i ≥ j → m = j)}
} else {
    {¬(i < j)}                            (3)  <--- added
    {(i < j → j = i) ∧ (i ≥ j → j = j)}   (4)
    m = j;
    {(i < j → m = i) ∧ (i ≥ j → m = j)}
}
{(i < j → m = i) ∧ (i ≥ j → m = j)}

表示するために残っているのは、2 つの連続するアサーションの場合です。最初のアサーションは 2 番目のアサーションを意味します。(これらは通常、「証明義務」と呼ばれます。) このような義務には、 should (1)Imply(2)と(3)should Implyの 2 つがあり(4)ます。これは明らかに事実です。

-- "qed" :-)

proof - 形式論理の正しさの証明

1 に答える 1

Related

Reference