3

コンパイラーがコンパイル時に dbc を強制できることを読みました.どのようにそれを行うのですか?

4

5 に答える 5

5

私の知る限り、これまでで最も強力な静的 DbC 言語は、Microsoft Research による Spec#です。ブギーと呼ばれる強力な静的分析ツールを使用し、 Z3と呼ばれる強力な定理証明/制約ソルバーを使用して、設計時に契約の履行または違反を証明します。

Theorem Prover がコントラクトが常に違反されることを証明できる場合、それはコンパイル エラーです。Theorem Prover がコントラクトが決して違反されないことを証明できる場合、それは最適化です。コントラクト チェックは最終的な DLL から削除されます。

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

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

于 2009-01-07T02:52:35.630 に答える
1
于 2009-01-06T23:29:00.347 に答える
1

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

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

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

于 2009-01-06T23:38:01.933 に答える
0

どのコンパイラとどの言語ですか? エッフェルはそれをある程度行うことができます。ただし、契約による設計を完全に実施することは、停止問題を解決できることを意味することを覚えておいてください (証拠: それを実行できるコンパイラがあると仮定します。その場合、コンパイラは、真の終了条件を持つ任意の関数を識別できなければなりません。無限ループまたは無限再帰のために終了条件を達成できない. したがって、停止に陥ります.)

これが通常意味することは、あなたが電話をしている場合

  foo(a);

そしてどこかで定義する

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

次に、コンパイラは、a が実際に開区間 (0..128) にあることを確認できます。

于 2009-01-06T23:27:01.100 に答える
0

Dのような一部の言語には、かなり強力なコンパイル時の定数の折りたたみとコンパイル時の条件チェックがあります ( Dstatic assert(boolCond, msg);の場合、IIRC C/C++ では#ifandpragmaまたはを使用できます#error) 。

于 2009-01-07T00:41:46.940 に答える