問題タブ [loop-invariant]
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.
127 問題
0
投票する
1
に答える
447
参照
c - frama-c wpの計算で反復ループを証明する方法は?
配列セル内の各桁の表現に 2 つの long 整数を追加する (WP ループの不変条件を調べるための) テスト コードがあります。
最後のループの不変条件のみを指定したい。\at(a[i], LoopCurrent) を使用して ACSL コードをいくつか試しました。不明なステータスまたはタイムアウトを受け取りました。最後に、成功せずに公理的再帰ソリューションを終了しました。
これを確認するために他に何を試みるべきか、今のところわかりません。ヘルプ？
更新: 実際の計算用の関数を作成しました。改善された公理。まだタイムアウトステータスを取得しています。opam の Frama-C 最新リリースをデフォルト設定 (タイムアウト = 10、証明者 Alt-Ergo) で実行しました。