問題タブ [formal-verification]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
insert - Dafny 挿入メソッド、事後条件がこのリターン パスで保持されない可能性があります
長さ「l」の文字列が含まれる配列「line」と、長さ「p」の文字列が含まれる配列「nl」があります。注: "l" と "p" は、対応する各配列の長さである必要はありません。パラメーター "at" は、挿入が "line" 内で行われる位置になります。再開: 長さ "p" の配列が "line" に挿入され、位置 (at,i,at+p),'p' の位置の間で "line" のすべての文字が右に移動して挿入されます。
保証の私のロジックは、「行」に挿入された要素が同じ順序であり、「nl」に含まれる文字と同じであるかどうかを確認することです。
コードは次のとおりです。
これが私が受け取っている エラーです。
ありがとう。
induction - 配列の領域をシフトする Dafny メソッドの検証
私は Dafny を使用して、あなたが受け取る削除メソッドを作成しています:
文字配列
line配列の長さ
l位置
at削除する文字数
p
最初に at から to までの行の文字を削除し、次にtoat + pの右側のすべての文字を移動する必要があります。at + pat
たとえば、[e][s][p][e][r][m][a]、 、at = 3、およびp = 3がある場合、最終結果は次のようになります。[e][s][p][a]
私は次のような意味のある事後条件を証明しようとしています:
ensures forall j :: (at<=j<l) ==> line[j] == old(line[j+p]);
at + p の右側からのすべての文字が新しい位置にあることを確認します。
しかし、Dafny は 2 つのエラーを出力します。
範囲外のインデックス 7 53
このリターン パスでは事後条件が保持されない可能性があります。19 2
formal-verification - Dafny にシーケンスで誘導を実行するように促すにはどうすればよいですか?
ダフニーを通過させるために、以下に何を追加する必要があるのだろうか？
formal-verification - Dafny での検索と置換の終了手段を見つけるには?
検索、削除、および挿入メソッドを使用する検索および置換メソッドをコーディングしています。while ループ内でこれら 3 つのメソッドを呼び出していますが、どの前提条件を使用すればよいかわかりません。
完全なコード:
system-verilog - システム Verilog アサーションでプロパティを書き込む方法は?
動作を正式に検証するために、SVA にプロパティを記述したいと考えています。
これが私がしたいことです：
sig1 が落ちた後、残りの評価サイクル中に LOW のままになるように、上記のプロパティを書き換えるにはどうすればよいですか?
注: sig1 をディセーブル iff (sig1) として配置したくありません。
verification - フォーマルツールの評価
3 つの正式な検証ツールを比較するために考慮すべき要素は何ですか? 例: Jaspergold、Onespin、Incisive。
私のちょっとした調査によると、Jaspergold が一番です。しかし、私はプロジェクトで自分でやりたいです。
1. サポートされている言語 (vhdl、sv、verilog、sva、psl など) 2. GUI 3. 機能 (どれだけ大きなデザインを処理できるか) 4. 評価サイクルの数 5. パフォーマンス (証明や反例を見つける速度）
このリストを拡張できる他の機能は何ですか?
ありがとう！
compiler-errors - この (配列) フィールドを操作するときにループ不変式が十分に強くない
更新しました
特定のクラスとそれぞれのメソッドを使用して以下に説明する、いくつかのダフニーの問題を解決する際の問題。他に何か必要な場合は、教えてください。事前に感謝します。また、rise4fun のこのすべてのコードでリンクが更新されます。
z3 - Equivalent of "store" operator for Records in z3
I am wondering if there is an operator for Records in z3 similar to the "store" operator for arrays. That is, given a record, is there any way to return a new record in which we've changed one element and all other elements retain their values? For instance:
The last line above is an example of what I would like to do. Is there any way to do this? Or is the user-defined constructor the only means to construct a new record? Thank you.
functional-programming - VHDL 関数呼び出し: 外部参照が未解決のままです
アーキテクチャ内で次のように機能します。
この関数が期待どおりに動作することを確認したいと思います。だから私は私のSVAファイルに同様の（正確ではない）関数を書きました。
しかし、エラーが発生します:「外部参照関数は未解決のままです」
アサーション ファイルに外部参照を追加するにはどうすればよいですか?
system-verilog - 正式な検証のためのプロパティの書き方は?
iff sig1=1'b1最初のクロック サイクルの後にプロパティを無効にしたい。
ハイからローへの移行sig1が私のトリガー条件です。私が行うと、disable iff(sig1)トリガー条件が満たされなくなります。
またthroughout、正式な検証者の有効化シーケンスと満足シーケンスの両方で使用することはできません。
どうすればできますか？ありがとう！