問題タブ [formal-verification]

私は Dafny でのレンマの使用を見てきましたが、理解するのが難しいと感じており、明らかに以下の例は検証されていません。これはおそらく、Dafny が帰納法またはカウントのいくつかのプロパティを証明するためのレンマのようなものを見ていないためです。 ? 基本的に、カウントが帰納的であるなどのことを Dafny に納得させるために、何をどのように定義する必要があるのか​​ わかりません。保証と不変条件の仕様の一部は必要ありませんが、それは重要ではありません。ところで、これは Spec# の方が簡単でした。

次の C コードがあるとします。

初期化時に変数 x の境界を静的分析を使用して計算したいと思います。これにより、満足のいく述語が得られます。この例では、メインの開始時の x の間隔は [8, 12] である必要があります。

TL;DR:コードのどこかにアサーションがある場合、これらの範囲を計算する最良の方法は何ですか?

私がこれまでに試したこと：

これにアプローチする最善の方法は、最も弱い前提条件計算機を使用することだと思います。私は frama-c の wp プラグインをいじってみましたが、検証目的で構築されているため、このユース ケースでどれほど役立つかはわかりません。次のコードにプラグインを適用する場合:

次の述語が代替エルゴ ソルバーに送信されます。

注意深く見ると、結果が (i_1 = 0) にならない変数 i の境界に従うことで、入力に必要な間隔を識別することができます。私はこれらの境界をマークしました。これはあまり堅牢ではありません。たとえば、アサーションが&& n <= 13に変更された場合、暗黙の述語の「左側」は変更された条件がないため同じままです。また、関数を呼び出すときにアサーションをrequireステートメントに変更するなど、他のシナリオでこれがどれほど役立つかはわかりませんが、結果の述語を理解できません:

そして、require ステートメントを関数に追加します。

私は得る：

私は正式な検証について読んでいますが、基本的なポイントは、正式な仕様とモデルを使用する必要があるということです。ただし、多くの情報源は静的解析を正式な検証手法として分類しており、一部は抽象的な解釈に言及し、コンパイラでの使用に言及しています。だから私は混乱しています-モデルの正式な説明がない場合、これらはどのように正式な検証になるのでしょうか?
編集：私が見つけたソースは次のとおりです：

静的分析: 定義済みの抽象化に従って、プログラム テキストから抽象セマンティクスが自動的に計算されます (ユーザーが自動/手動で調整できる場合もあります)。

では、正式な仕様を必要とせずにソース コードだけで動作するということですか? これは、静的アナライザーが行うことです。

また、正式な検証なしで静的解析は可能ですか? たとえば、SonarQube は本当に正式なメソッドを実行しますか?

最近、私は正式な検証について多くのことを読んでいて、このトピックに魅了されています。しかし、私は次のことを理解できません:
正式な検証には正式な仕様が必要ですが、プログラムの正式な仕様がない場合、コンパイラのソース コードでどのように抽象的な解釈を使用できますか?

正しいと思われる外国語のテキストからの翻訳 (また、正式な仕様は必要ないようです)。

プログラムがその制御フロー チャートによって表される場合、各分岐はプログラムの状態を表し (複数の場合があります。たとえば、ループでは分岐が複数回通過します)、抽象的な解釈により、この状態のセットに近似する静的セマンティクスが作成されます。

正式な検証手法としての抽象的な解釈に関する記事: http://www.di.ens.fr/~cousot/publications.www/Cousot-NFM2012.pdf

私は Windows OS を使用しており、Cygwin i で次のように入力wish -f ispin.tclして ispin インターフェイスを開きます。test.pml以下を含むファイルを開きます。

その後、シード = 123 でランダムな方法を使用して実行します。結果は問題なく出力に出力されます。

このモデルを検証しようとすると、問題が発生します。検証の結果は次のとおりです。

どうすればこれを解決できますか? インターネットで検索しましたが、役立つ情報が見つかりませんでした。

注：検証プロパティは変更していません：

line長さ の文字列が含まれる配列があります。これはl、 pat長さ の文字列が含まれる別の配列ですp。注:pとlは配列の長さではありません

目的は、に含まれる文字列が にpat存在するかどうかを確認することですline。その場合、このメソッドはline単語の最初の文字のインデックスを返し、そうでない場合は を返す必要があり-1ます。

「トリガーする用語が見つかりません」というエラーを引き起こしている不変条件はensures exists j :: ( 0<= j < l) && j == pos;、invariant forall j :: 0 <= j < iline ==> j != pos;

ループの私の論理は、それらがループ内にある間、インデックスが見つからなかったということです。そして、確実なのは、インデックスに遭遇したときです。

何が間違っている可能性がありますか？

コードは次のとおりです。

次のエラーが表示されます: Dafny 出力のスクリーンショット

これが rise4funのコードです。

長さ「l」の文字列が含まれる配列「line」と、長さ「p」の文字列が含まれる配列「nl」があります。注: "l" と "p" は、対応する各配列の長さである必要はありません。パラメーター "at" は、挿入が "line" 内で行われる位置になります。再開: 長さ "p" の配列が "line" に挿入され、位置 (at,i,at+p),'p' の位置の間で "line" のすべての文字が右に移動して挿入されます。

保証の私のロジックは、「行」に挿入された要素が同じ順序であり、「nl」に含まれる文字と同じであるかどうかを確認することです。

コードは次のとおりです。

これが私が受け取っている エラーです。

ありがとう。