問題タブ [formal-verification]

C で strlen のような関数を証明しようとしていますが、frama-c は事後条件とloop variant len節を証明しません。理由がわかりません！

私が試したこと：

私は何を間違っていますか？

純粋な 関数は、数学関数に似た関数であり、「実世界」との相互作用も副作用もありません。より実用的な観点からは、純粋な関数では次のことができないことを意味します。

• メッセージを印刷または表示する
• ランダムにする
• システム時刻に依存
• グローバル変数を変更する
• その他

このすべての制限により、非純粋関数よりも純粋関数について推論する方が簡単になります。プログラムのバグが少なくなるように、大部分の関数を純粋にする必要があります。

Haskell のような巨大な型システムを持つ言語では、読者は関数が純粋かどうかを最初からすぐに知ることができるため、後続の読み取りが容易になります。

@purePython では、この情報は、関数の上に置かれたデコレーターによってエミュレートされる場合があります。また、そのデコレーターが実際に検証作業を行うことも望んでいます。私の問題は、そのようなデコレータの実装にあります。

今のところ、関数のソース コードを調べて、または、または、およびそれらのいずれかが見つかった場合に不平を言うなどの流行語をglobal探しrandomますprint。

しかし、あなたの運次第でうまくいくかもしれないし、うまくいかないかもしれない奇妙なハックのように感じます。より良いデコレータを書くのを手伝ってくれませんか?

完全宣言型ホーン ロジック(または完全宣言型プロローグ)と呼ばれるもので、いくつかの知識を形式化し、クエリを実行したいと考えています。誰かがそれを実装する方法に関するガイドラインを提供できますか? 上記のリンクからの詳細な説明を簡単に要約します。

正式な言語は、Prolog (のコア) のものです。「プログラム」は、Prolog と同様に、規則と事実のセットです (関数と変数を含み、基本的にはユーザー定義の述語のみを含みます)。

ただし、Prolog とは対照的に、論理プログラムの標準的な宣言的セマンティクスに関して健全で完全な実装、つまり最小の Herbrand モデル (帰納的に定義された基本用語のセット) を探しています。論理プログラミングの理論的研究では、これは通常研究の対象であり、たとえば、次の条件:

• マッチング ルールの公平な検索 (たとえば、Prolog の深さ優先検索は公平ではありません)。
• "発生チェック" による統一 (変数が統一された項に出現しないことを確認する)。

車輪を発明するのではなく、既存の機能に基づいて構築される簡潔な実装を探しています。私が見ているより有望な方向性の 2 つは、Prolog のメタインタープリターとして、または何らかの定理証明の一部として実装することです。これらの分野で実際的な知識を持っている人は、それを実装する方法に関するガイドラインを提供できますか? miniKanrenで簡単に実装できますか?

私の意図は、一部の知識を完全に宣言的な方法で形式化することです。このような形式化の重要な特徴は、それが (単調な) 帰納法の数学的概念に正確に対応しているため、知識とその特性を帰納的な議論で簡単に推論できることです。

リストがあるとします：

変更可能なリストについて話していることに注意してください。そして、自明な再帰的な長さ関数:

当然、リストが非循環の場合にのみ終了します。

この述語は、再帰関数として実装されているため、循環リストで終了しないことに注意してください。

通常、リストの長さを有界の減少要因として使用するリスト トラバーサル終了の証拠を目にします。Length彼らはそれが非負であると考えています。しかし、私が見る限り、この事実 ( ) はそもそもLength l >= 0の終了から導かれます。Length

が終了し、 （または同等の、より適切に定義された述語）リストでLength非負であることをどのように証明しますか?NonCircular

ここで重要な概念が欠けていますか?

ACSL で定義された帰納述語で帰納を使用することは可能ですか?

ACSL マニュアルの次の例を検討してください。

次の補題を証明しようとしています。

Alt-Ergo はここで失敗するので、手動の Coq 推論に頼ります。

しかし、 Iの場合Search P_reachable、次の 2 つの公理のみが生成されていることがわかります。

そして誘導原理はありません。だから応募できないinduction P_reachableとかdestruct P_reachable。

frama-cバージョン Sodium-20150201の WP プラグインを使用しています。

再現するには、との定義と補題frama-c -wp -wp-rte -wp-prover coqide file.cがfile.c含まれているを実行できます。Listreachablenext_null_reachable

\freeableそれが前提条件であることを考えると、ポインタが であることをどのように証明できますか?

割り当てが WP でまだ完全にサポートされていないのは結果ですか?

サポートされていない場合、WP が条件を生成するのはなぜtyped_fint_call_free_deallocation_pre_freeableですか? また、どうすれば破棄できますか?

PS私はナトリウムframa-cを使用しています。