問題タブ [alt-ergo]
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.
z3 - Alt-Ergo を使用して次の SMT-LIB コードを実行する方法
次の SMT-LIB コードは、Z3、MathSat、および CVC4 では問題なく実行されますが、Alt-Ergo では実行されません。どうなるか教えてください。よろしくお願いします。
z3 - 配列に対する関数の単純なプロパティの証明
次の注釈付き C コードがあるとします。
Z3 も Alt-ergo も、アサート final_a と事後条件を証明できません。Z3 はループ不変式も証明できません。
Alt-Ergo の出力:
Z3 の出力:
何が欠けている？
z3 - 強力な証明済みアサーションにもかかわらず、SMT 証明者は「不明」を生成します
次の C 注釈付きコードがあるとします。
final_progress ステートメントが証明されたにもかかわらず、Alt-Ergo/Z3 が「不明」または final_c アサーションのタイムアウトを生成するのはなぜですか? そのような明らかに（ユーザーの観点から）無効なステートメントについては、「無効」と表示したいと思います。
c - frama-c wp const 変数と const 配列
Frama-C の WP プラグインを使用していくつかの C コードを証明しようとしていますが、以下の例に問題があります。
指示：
私のframa-cのバージョンはSodium-20150201で、alt-ergoは0.95.2です
結果は
気がついたらいつ変わるんだろう
に
と
結果は
しかし、「requires STRING_LEN == 5;」に頼りたくありません。'const' を使用して最初の例を証明します。それを達成する方法は？
c - 述語を満たす入力の範囲を計算する
次の C コードがあるとします。
初期化時に変数 x の境界を静的分析を使用して計算したいと思います。これにより、満足のいく述語が得られます。この例では、メインの開始時の x の間隔は [8, 12] である必要があります。
TL;DR:コードのどこかにアサーションがある場合、これらの範囲を計算する最良の方法は何ですか?
私がこれまでに試したこと：
これにアプローチする最善の方法は、最も弱い前提条件計算機を使用することだと思います。私は frama-c の wp プラグインをいじってみましたが、検証目的で構築されているため、このユース ケースでどれほど役立つかはわかりません。次のコードにプラグインを適用する場合:
次の述語が代替エルゴ ソルバーに送信されます。
注意深く見ると、結果が (i_1 = 0) にならない変数 i の境界に従うことで、入力に必要な間隔を識別することができます。私はこれらの境界をマークしました。これはあまり堅牢ではありません。たとえば、アサーションが&& n <= 13に変更された場合、暗黙の述語の「左側」は変更された条件がないため同じままです。また、関数を呼び出すときにアサーションをrequireステートメントに変更するなど、他のシナリオでこれがどれほど役立つかはわかりませんが、結果の述語を理解できません:
そして、require ステートメントを関数に追加します。
私は得る：