design-by-contract - 契約による設計を使用する最も広く使用されているオープンソースプロジェクトは何ですか？

Question

エッフェルコミュニティの外で実際に契約による設計がどれだけ使用されているのか知りたいです。契約による設計を使用するアクティブなオープンソースプロジェクトはありますか？

または、質問を1つにまとめると、単一の答えがあります。契約による設計を使用する、最も広く使用されている（Eiffel以外の）オープンソースプロジェクトは何ですか？

Answer 1

あなたの質問の「エッフェル以外」の部分は興味深いものです。コントラクトは、プログラミング言語でサポートされている場合にすべての意味を持ちます。それ以外の場合は、コメントの優れた構文にすぎません。

これで、コントラクトをサポートする言語にたどり着きます。私はエッフェル以外の 3 つを知っています。

• ESC/Javaは、 JMLという名前の言語を使用して Java にコントラクトを追加します。
• すべての .NET 言語の.NET コントラクト(バイトコード レベルで動作)
• Frama-Cは言語ACSLを使用して C にコントラクトを追加します

最初の 2 つは実行可能な契約を持っています。利点: ランタイム アサーションとして使用できます。短所: 関数がコントラクトで何をするかを完全に指定する表現力が不足しています。基本的に、サニティ チェックのみを記述できます。

一方、ACSL コントラクトはより表現力があり、実行可能ではありません。これらにより、並べ替え関数が常に終了し、元の配列と同じ要素を順番に残す必要があることを完全に指定できます。ACSL コントラクトは、静的分析、特に Hoare スタイルの最弱前提条件の計算に使用できます。

最後のものだけはよく知っています (免責事項: 私は Frama-C に取り組んでいますが、ACSL の部分は多くの人々の仕事であり、その中には私よりもはるかに多くの貢献をした人もいます)、「ACSL by example"、現在 Fraunhofer FIRST によって開発されている ACSL コントラクトを持つオープン ソース C ライブラリです。まだリリースされていませんが、Device-softプロジェクトの一部としてリリースされる予定です。興味があれば、暫定版を入手できると思います。その最後の Web ページに連絡先として記載されている人に連絡してください。