問題タブ [formal-semantics]

ウィキペディアがリストするループ不変条件を考えると、ループの最も弱い前提条件を生成する良い方法 ( http://en.wikipedia.org/wiki/Predicate_transformer_semanticsから):

M[x <- N] は、M 内のすべての x を N に置き換えます。

さて、私の問題は変数 y です。\forall y, は式で y をバインドするため、「y は新しい変数のタプルです」は解析されません。"[x <- y]" の y と同じように、y は \forall でバインドされていますか? 上記を解析することはできません。

編集：参照要求を避けるために言い換えました。

私の質問は、ループ不変条件と最も弱い前提条件の計算との間の直接的な関係は何かということです。実際に行われている多くのことは、ループの最も弱い前提条件を検証に適した前提条件に緩和しているようです。ウィキペディアの上記は、ループ不変条件が与えられた場合、鼻の最も弱い前提条件を実際に計算できることを示唆していますが、この条件を理解するのに苦労しています。

プロセス a またはプロセス b がクリティカル セクションに入りますが、同時にではありません。これが発生した場合 (つまり、それらが同時にクリティカル セクションに入った場合)、割り込みが実行されます。

p = プロセス a

q = プロセス b

r = クリティカル セクション

演算子 ∨ = または

演算子 → = 含意

私の答え ：

(p ∨ q) → r

これは正しいですか、それとも私が何か間違ったことをしましたか? 命題論理を理解しようとしています。

私は正式な検証について読んでいますが、基本的なポイントは、正式な仕様とモデルを使用する必要があるということです。ただし、多くの情報源は静的解析を正式な検証手法として分類しており、一部は抽象的な解釈に言及し、コンパイラでの使用に言及しています。だから私は混乱しています-モデルの正式な説明がない場合、これらはどのように正式な検証になるのでしょうか?
編集：私が見つけたソースは次のとおりです：

静的分析: 定義済みの抽象化に従って、プログラム テキストから抽象セマンティクスが自動的に計算されます (ユーザーが自動/手動で調整できる場合もあります)。

では、正式な仕様を必要とせずにソース コードだけで動作するということですか? これは、静的アナライザーが行うことです。

また、正式な検証なしで静的解析は可能ですか? たとえば、SonarQube は本当に正式なメソッドを実行しますか?

私はK セマンティクス フレームワークを使用しており、チュートリアルを実行しています。これは私の TEST1.k です。

しかし、コマンド Kompile Test1.k を実行すると、次のエラーが発生します。

O'Reilly NLTK bookの Chapter 10に見られるように、「ボブはアリスを愛している」という文の構文ツリーをモデル化したい場合、つまり

一次論理ラムダ式に変換すると、次のようになります。

左側に型のツリーがあり、右側に λ 式のツリーがあります。Bob と Alice の両方を型上げすることにしました。

私の質問は次のとおりです。タイプのツリーから、「愛」のタイプが でなければならないことを簡単に計算できますが、<<<e,t>,t>,<e,t>>これから対応する λ 式が

λR.λx.R(λy.loves(x,y))

構文ツリーの葉の λ 式をその型と周囲の λ 式から取得する方法はありますか?