問題タブ [verifiable-c]
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.
verifiable-c - 前提条件の配列範囲
現在VSTの使い方を勉強中です。VST1.5を使用しています。私はこの小さな C プログラム ( backref.c) を持っています:
私のCoqコード（簡単な事前条件と事後条件付き）は
out[-dist]前提条件として、 toout[-1]は読み取り可能で、out[0]toout[length-1]は書き込み可能であると言いたいです。PLCC 210 ページに条件array_at_rangeが記載されていますが、VST 1.5 では使用できないようです。これどうやってするの？
verifiable-c - Xor-Swapping の正しさの証明
更新：今、私は次のプログラムを持っていますswap.c：
私の仕様は
今、私は立ち往生しています:私は展開することができ、展開eval_binopを進めようとしますが、実際には作業できるものに収束しません。さらに、`eq プロパティを使用して実際に何かを書き換える方法もわかりません。
verifiable-c - 機能仕様 Verifiable-c を指定する方法を見つける
私は検証可能な c の作業を始めたばかりで、自分が書いた C コードの機能仕様の生成に苦労しています。私が扱っている私の基本的な例は、単純に（Cコード）です
定義 xor_spec セクションをまとめるのに苦労しています。
ありがとう。
coq - ローカル変数を使用した forward_call
VST バージョン 1.7。
関数呼び出しで変数を使用しようとすると、coq がローカルで宣言された変数を認識しないという問題があります。私はコードを持っています：
coq タイプのビット: リスト Z、invKey: Z、サイズ: Z。
bit = bits[i] ステップを正常に実行しましたが、次に使用して前進しようとすると
このステップは、環境内でビットが見つからずに失敗します。使ってみた
_bit が LOCAL 句に表示されますが、_bit は int または Z 型ではなく ident 型であるため、型の不一致が生じます。結果として、ローカルで定義された値を使用して他の関数を呼び出す方法を考えているので、助けていただければ幸いです。
verifiable-c - 検証可能な c を使用してグローバル変数の分離仕様を記述する方法
以下は、C でのコード例です。
検証可能な c (vst) を使用して機能仕様を記述しましたが、検証の最後に「typecheck_error (deref_byvalue tint)」というエラーが発生します。上記の c 関数の正しい founc 仕様を書く方法を教えてくれる人はいますか? ポイントはグローバル変数のSEP()の書き方です。
（ここは間違っています、訂正してください）