コード契約 - 事前および事後条件についてプライベートメソッドをチェックする必要がありますか？

Question

私はコード契約のスピードを上げようとしています。私はコンセプトが好きですが、実際にはContractを追加する価値はありません。いくつかのプライベートメソッドで必要です。

私はパブリックメソッドのポイントを見ることができますが、プライベートクラスのメソッドでは、それは過剰なようです。

Answer 1

主な理由です。あなたはプライベートメソッドについて暗黙の仮定をするコードを書くことがよくあります（このメソッドはnullを返しません）、静的証明者はこれをあなたに指摘します。仮定をパブリックメソッドの本体に入れたり、プライベートメソッドの契約として追加することができます。後者は一般的により洗練されています。それは、そのプライベートメソッドの複数の使用を通じて契約によって暗示された仮定を再利用できるようにするためです。

個人的には、もう少し成熟するチャンスが得られるまで、私はコード契約をあきらめました。構文は厄介です（特に、null値のないパラメータを単純に表現する必要があります）、複雑なシステムを静的に証明しようとする多くの回転を経験することができます。しかし、非常に良いアイデアだと思います。洗練された静的解析のための適切な契約サポートが.NET（実際のCILメタデータ）に焼き付けられ、厄介な拡張機能ではなくC＃でのネイティブ言語サポートが提供されるまでは、時間の問題です。 。

私は、プライベートとパブリックのメソッドを含め、上から下へ小さなアプリケーションに契約を適用するプロセスを進めることは非常に価値があると思います。あなたがすべてを証明するプロセスを進めるにつれて、それを実現さえせずに毎日行う暗黙の前提の多くが明らかになります。契約書を設計する際に育った考え方は、仮定を立てているポイントを強調し、仮定が時々違反されるかどうかを検討するように奨励しているため、私は日々の仕事でこれを行う予定の時間がありませんが、コード契約を試していた時期からずっと学んだことは間違いありません。

Answer 2

通常、契約はパブリックメソッドの前後でのみチェックされます。プライベートメソッドは、パブリックメソッドの呼び出しの一部としてのみ呼び出されるため、個別にチェックする必要はありません。あなたは静的解析を利用している場合は、プライベートメソッドに契約を適用したいと思います

http://en.wikipedia.org/wiki/Class_invariant