問題タブ [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 - 解釈できない関数 (合同分析) の理論はありますか?
私はシンボリック変数のセットを持っています:
いくつかの公理によって制約される一連の未知の関数:
ここで関数f1、f2、f3は不明ですが、修正されています。したがって、それは の理論ではありませんuninterpreted functions。
次の主張の妥当性を証明したい:
上記の公理的等式に基づく置換を使用します。
関数の解釈を考え出すのではなく、提供された等式のみを使用して答えを結合しようとするような定理の理論はありますか?
もしそうなら、その理論の名前は何ですか? また、どの SMT ソルバーがそれをサポートしていますか?
線形算術のような他の理論と混合できますか?
frama-c - ユーザー エラー: 証明者 'alt-ergo' が why3.conf に見つかりません
Frama-c で関数をテストしようとしています:
すべての要件をインストールした後: OPAM、why3、alt-ergo frama-c -wp fct.cを実行するたびに、次のメッセージが表示されます。
frama-c - Frama C で Alt-ergo を使用して WP を証明している間のタイムアウト
Frama-cを使用して以下のプログラムの正確性を検証しようとしていました私はframa-Cの新しいユーザーです。
問題：
従業員の基本給を入力し、以下に従って総給与を計算します。
基本給 <= 10000 : HRA = 20%、DA = 80%
基本給 <= 20000 : HRA = 25%、DA = 90%
基本給 > 20000 : HRA = 30%、DA = 95%
私はここでどんな間違いをしていますか？前提条件をより正確にする必要があります。
コンソール メッセージ: