6

これを書くと：

public sealed class Foo
{
    private int count;
    private object owner;
    private void Bar()
    {
        Contract.Requires(count > 0);
        Contract.Ensures(owner == null || count > 0);

        if (count == 1)
            owner = null;
        --count;
    }
}

静的コントラクト チェッカーは、すべてのアサーションを証明できます。

しかし、代わりにこれを書くと：

public sealed class Foo
{
    private int count;
    private object owner;
    private void Bar()
    {
        Contract.Requires(count > 0);
        Contract.Ensures(owner == null || count > 0);

        --count;
        if (count == 0)
            owner = null;
    }
}

owner == null || count > 0事後条件が証明されていないと主張しています。

2 番目の形式がこの事後条件に違反していないことを証明できると思います。

// { count > 0 } it's required
--count;
// { count == 0 || count > 0 } if it was 1, it's now zero, otherwise it's still greater than zero
if (count == 0)
{
    // { count == 0 } the if condition is true
    owner = null;
    // { count == 0 && owner == null } assignment works
}
// { count == 0 && owner == null || count != 0 && count > 0 } either the if was entered or not
// { owner == null || count > 0 } we can assume a weaker postcondition

私の証明に何か問題がありますか？

証明にアサーションをContract.Assertコードへの呼び出しとして追加し、これだけを追加すると事後条件を証明できるという結論に達しました。

--count;
Contract.Assert(count == 0 || count > 0)
if (count == 0)
    owner = null;

しかし、同じアサーションを「より自然な」方法に変更すると、失敗します。

--count;
Contract.Assert(count >= 0)
if (count == 0)
    owner = null;

これら 2 つのアサーションは同等であると予想されますが、静的チェッカーはそれらを異なる方法で扱います。

(ちなみにVS10のベータ2を使っています)

4

2 に答える 2

1

結局のところ、この非常に複雑な証明器が完全に機能する状態になるとは思っていません。これはバグであるか、少なくとも開発者に報告する価値があるポイントだと思います。なぜなら、これは自動的に静的チェックを行うための非常に簡単なことだからです。

とにかく、一見すると、静的コントラクト チェッカーが条件を保証できるかどうかを確認するためだけに、ensure マーカーが存在します。これは、条件が無効であることを意味するのではなく、証明が見つからないことを意味します。

無効なものが保証されていると書かれている場合は、もっと心配です。 それはバグとしてカウントされます！

于 2009-12-17T17:34:11.347 に答える
0

警告: 私は .net コントラクト システムの詳細についてまったく知りません。

ただし、これだけは言えます。このシステムがサポートしているように見えるほど豊富なアサーションの完全な証明者を作成することは、文字通り不可能です (停止問題を参照)。

だから：これはバグですか？いいえ。

一方、これは、証明者の実装者がシステムに追加したいと考える一般的なケースである可能性があると示唆するのはもっともらしいようです。

于 2009-12-17T17:17:43.363 に答える