問題タブ [kframework]
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.
kframework - K でグローバル状態を操作するステートフル ルール?
K には、ルールがアクセスできるグローバル状態の概念がありますか? 例: 構成を言いますC => C'。C'探索済みの状態のセットに存在しない場合に遷移し、探索済みの状態のグローバル セットを追加C'して更新します。
プログラムの到達可能なすべての状態を非決定論的に ( --search オプションを使用して) 調査しようとしています。ただし、探索される各パスは独立しています。つまり、構成自体で探索されたセットを渡す場合、各パスは他のパスに見られる構成を認識しません。
グローバルな状態がない場合、この種の動作のベスト プラクティスは何ですか? それぞれの独立したパスがアクセスできるより大きな環境内で遷移を非決定論的に調査する方法はありますか?
kframework - #as? などの # キーワードのドキュメント
などの利用可能なキーワードとその使用方法に関するドキュメントはどこかにありますか#as?
具体的には、セットまたはその中に含まれるセルと等しいことを#as意味<k> S:Set </k> #as ASETしますか?ASETkS
構文は<k> ... SetItem(X) ... #as S </k>有効ですか?
kframework - K で [バインダー] を使用するには?
私は構文を持っています：
2 つの構文には、異なるバインドを行う 3 つのプロダクションがあります。
a(x).P、ここでxは に拘束されてPいaますが、その用語に拘束されていない名前です。new a.Pラムダのようにバインドaします。Pf(a,b,c) = Pinのベクトルa,b,cをバインドします。ベクトル内のそれぞれは にバインドされているはずです。KVarPKVarP
binderプロダクションで特定の変数をバインドするように指示するにはどうすればよいですか? 2番目がバインドされているはずだbinder(2)と伝えるようなものはありますか? KVarいくつかKVarの が別の構文で定義されている場合はどうなりますか?
kframework - Kフレームワークで「krun」に文字列引数を渡す方法は?
K フレームワークでは、 の-cスイッチを使用しkrunて、他の変数を初期設定に渡し、次に default を渡すことができます$PGM。たとえば、次のコードがある場合があります。
と実行するkompile imp.k; krun tests/sum.imp -cSOMEARG=3と、$SOMEARG変数は値を取得します3。ただし、文字列を渡そうとすると問題が発生します。
の後kompile、コマンド
出力:
文字列引数を渡すにはどうすればよいですか?