問題タブ [why3]
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.
formal-verification - Why3 の述語で自分の関数を呼び出す
Why3 (1.0.0) の最新バージョンで、次のようなことをしようとすると:
次の形式のエラーが表示されます: File "../something.why", line x, characters yz: unbound symbol 'add_one'. 私は何か間違ったことをしていますか？私が見た WhyML コードのほとんどの例は、実際には組み込み/標準ライブラリ関数のみを使用していますが、同じファイルで定義された他の述語を呼び出しています。述語を定義するときに、同じファイルで定義した関数を呼び出す同様の方法はありませんか?
frama-c - ユーザー エラー: 証明者 'alt-ergo' が why3.conf に見つかりません
Frama-c で関数をテストしようとしています:
すべての要件をインストールした後: OPAM、why3、alt-ergo frama-c -wp fct.cを実行するたびに、次のメッセージが表示されます。
macos - Frama-C 23 と Coq
Frama-C (23)、Why3、および Coq を macOS にインストールした後、次のコマンドを実行しました
以下のメッセージが表示されました
- これは Frama-C で coq を使用できないということですか?
- 上記のWhy3ライブラリをコンパイルするようにopamに指示するにはどうすればよいですか?
よろしく