3

少し前に C の形式仕様言語について何かで読んだ記憶がありますが、今は必要なため見つけられません。

これは JML に触発されたもので、私が見た限りでは同じ構文を使用していました。

私が見つけた唯一の参照は論文ですが、私が話しているのはそれよりも洗練されたものです.

これがあなたに鐘を鳴らしたら...

誰もこれについて知らない場合は、C で正式な検証と自動テスト生成を行う方法についてお知らせいただければ幸いです。

前もって感謝します。

4

3 に答える 3

1

私はCMLに精通していませんが、リンクする記事は、非機能要件の仕様に関するものであるというステートメントから始まります。

JMLはJavaプログラムの機能要件のためのものです（わかりました、線はぼやけていますが、CMLの記事ではこの文と同じ意味でこの単語を使用していると思います）。Cプログラム用のJMLに相当するもの（したがって、純粋に機能要件用）はACSLです。

フォーマル検証の場合、私はFrama-Cのみを推奨できます（免責事項：私はFrama-Cに取り組んでいますが、ACSL仕様に関係する部分には取り組んでいません）。Cプログラムのテスト生成については、CUTEについて良いことを聞いたことがあります。

于 2010-10-13T12:48:44.393 に答える
0

Cの「for」の正式な仕様？

私は、Cを正式に指定する作業を知っています：Cの表示的意味論。

Cプログラムの機能を指定する場合は、プロパティ仕様言語から始めると便利です。

于 2010-11-10T12:09:47.263 に答える
0

C には少なくとも 4 つの検証システムがあります。

  1. エッシャー C 検証ツール。【私はこれでつながっています。】
  2. マイクロソフト VCC .
  3. Frama-Cと Jessie プラグイン (パッケージ内の Debian/Ubuntu で利用可能。jessie を機能させるには、これもframa-cインストールする必要がありますwhy)
  4. ベリファスト。

(1) は、MISRA-C などで書かれた安全性が重要な組み込み C プログラムを対象としています。(2) は、Microsoft C コンパイラを使用して構築されたマルチスレッド システムを対象としています。(3) と (4) についてはあまり知りません。

于 2011-02-10T00:55:56.890 に答える