私はCプロジェクトのいくつかに取り組んでいます。コードの検証に自動定理証明を使用したいと思います。理想的には、ATPを使用して関数契約を検証するだけです。 design by contractスタイルのコーディングを可能にするC/gccや外部ソフトウェア/パッケージ/ etcの機能はありますか？自動定理証明で使用するためのCでの契約による設計
もしそうでなければ、それだけで私自身で始めることができます。
私のリファレンスはMSRのSpec＃やSing＃のようなものですが、私はオープンソースの人で、オープンソースのソリューションを探しています。
明らかに、それは言語に組み込まれていませんが、あなたに行くためのアドオンがたくさんあります。彼らのほとんどはベータ版ですが、あなた自身のものよりもむしろ貢献することを検討するかもしれません。
RubyForgeのもの、Design by Contract for Cは非常に有望です。 GNU Nanaは長い間ご使用いただいており、おそらくお客様のニーズに合っています。これらが役立つことを願っています。
編集：Cのためにデザインすることで契約にthis article at O'Reilyをチェックアウト：アサート（）と契約による設計興奮 と
満足していない、私はのための 契約の実装で自分のデザインを作成するために着手した C. の後にいくつかのソリューションを見て Java 1私は に契約を表現するためにオブジェクト制約 言語のサブセットを使用することにしました[4]。 RubyとRaccを使用して、 のC言語コードに埋め込まれたコントラクトを コントラクトをチェックするCコードに変換するコード生成器 を作成しました。
定理証明者を使用してCコードの検証に興味がある場合は、VCC projectを確認する必要があります。 ウェブサイトから：
VCCは、並行Cプログラムの機械的検証プログラムです。 VCCは、関数指定、データ不変式、ループ 不変式、およびゴーストコードで注釈を付けられたC プログラムを受け取り、これらの注釈を正確に証明しようとします 。成功した場合、VCCはプログラムが実際に の仕様を満たしていることを保証します。
VCCは、Microsoft Researchから非常に成熟したシステムであり、Microsoft Hyper-Vのハイパーバイザを検証するために使用されています。 VCCもオープンソースです。