ノート:ホーア論理

色々と疑問点

• 「部分的に正当（partially correct）であると言い、P { S } Q と記述する」とありますが、部分的に正当でないときには P { S } Q と書くのも禁止ということでよろしいですか？この場合に、書き間違えていないことを確認するにはどうすればいいのでしょうか？
• 例の項目の例1の { x = 42 } y := x + 1 { y = 43 ∧ x = 42 } は何をどうしたら出てきたのでしょうか？
• 「例えば、以下の例で x と y が同じ値を参照している場合$\{A\}\ x:=2\ \{y=3\}$この Triple は真ではない。」の同じ値を参照してるというのは何ですか？また、真ではないというのは何ですか？Aが何なのか分かりませんが、Aの代わりにfalseと書いてあっても「真」ではないのですか？
• 置換と代入は何が違うのですか？ --153.204.209.174 2016年4月30日 (土) 11:14 (UTC)

• 本人ではないですが、代入は対象プログラム内のステートメントについて言ってるのに対して、置換は表明の方について言っているのでは。統一されているかは確認してないですけど。 --しんのすけ代表（会話） 2019年11月7日 (木) 04:22 (UTC)