このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

対話ホーア式 改

論理 プログラム意味論

Cond+(Σ) = Form(Obs(Σ+))（内部条件；直接制御可能）、Cond-(Σ) = Form(Obs(Σ-))（外部条件；直接制御不可能、コマンド経由）だとする。

P∈Cond(Σ), Q∈Cond+(Σ), R∈Cond-(Σ), F∈Cmd(Σ), E∈Evt(Σ)に対して、次の形を持つ。メッセージは中括弧にする。

  • when(P) sending{F} results(R) causes{E}.
  • when(P) receiving{E} changes(Q) motivates{F}.

なんなら：

  • when (P), sending{F} changes you(R) causes your{E}.
  • when (P), receiving{E} changes me(Q) causes my{E}.