Design by Contractでのコンパイル時チェック？

StackOverflow https://stackoverflow.com/questions/418588

  •  03-07-2019
  •  | 
  •  

質問

コンパイラはコンパイル時にdbcを強制できると読みました。どのように実行しますか？

役に立ちましたか？

解決

私が知る限り、これまでで最も強力な静的DbC言語は Microsoft Researchの仕様＃。 Boogie という強力な静的分析ツールを使用します。このツールでは、<< href = "http://Research.Microsoft.Com/projects/z3/" rel = "noreferrer"> Z3 を使用して、設計時に契約の履行または違反を証明します。

定理証明者が契約に常に違反することを証明できる場合、それはコンパイルエラーです。定理証明者が契約に違反しないことを証明できる場合、それは最適化です：契約チェックは最終DLLから削除されます。

チャーリー・マーティンが指摘するように、一般に契約を証明することは停止問題を解決することと同等であり、したがって不可能です。そのため、定理証明者が契約を証明することも反証することもできない多くの場合があります。その場合、他のより強力でないコントラクトシステムと同様に、ランタイムチェックが発行されます。

Spec＃は現在開発されていないことに注意してください。契約エンジンは、 Code Contracts for .NET というライブラリに抽出されました。これは一部になります.NET 4.0 / Visual Studio 2010の。ただし、契約の言語サポートはありません。

他のヒント

コンパイラは、静的分析を使用してプログラムを調べ、実行するかどうかを判断できます。正しいこと。簡単な例として、次のコードは負の数の平方根（C ++）を取得しようとします。

double x;
cin >> x;
cout << sqrt(x) << endl;

コンパイラが sqrt が負の数で呼び出されるべきではないことを知っている場合、ユーザー入力からの読み取りが 負の数。一方、これを行う場合：

double x;
cin >> x;
if (x >= 0) {
    cout << sqrt(x) << endl;
} else {
    cout << "Can't take square root of negative number" << endl;
}

その後、コンパイラは、このコードが負の数で sqrt を呼び出すことは決してないことを知ることができます。

契約による設計は、非常に抽象的な用語です。表現力の異なる多くの仕様形式が存在する可能性があるためです。さらに、現在、仕様を確認および実施する静的分析の能力には制限があります。これは、コンピューターサイエンスで最も活発な学術および産業研究分野の1つです。

実際には、コントラクトとチェックのサブセットを使用する可能性が高く、使用する言語とインストールするプラグインまたはプログラムによって異なります。

一般に、静的分析では、契約のモデルと実際のプログラムのモデルを構築し、それらを比較しようとします。たとえば、オブジェクトが状態Sにあるときにコントラクトで関数を呼び出せない場合、呼び出しシーケンスで状態Sになる可能性があるかどうかを判断しようとします。

どのコンパイラとどの言語ですか？エッフェルはある程度それを行うことができます。ただし、契約による設計を完全に実施することは、停止問題を解決できることを意味することを忘れないでください（証明：できるコンパイラがあると仮定します。その後、コンパイラは、真の終了条件で任意の関数を識別できる必要があります。無限ループまたは無限再帰のために終了条件を達成できません。したがって、停止になります。

これが通常意味するのは、電話がある場合

  foo(a);

および他のどこかで定義

  function foo(a:int) is
     assert 0 < a && a < 128
     ...
  end

その後、コンパイラはaが実際にオープン間隔（0..128）になることを確認できます。

D などの一部の言語は、適度に強力なコンパイル時定数の折りたたみとコンパイル時の条件チェック（ D static assert（boolCond、msg）; 、IIRC C / C ++は #if と pragma または #error ）

ライセンス： CC-BY-SA と 帰属
所属していません StackOverflow
scroll top