わりとわかりにくくて混乱しやすい気がするホーア論理の代入の規則ですが,見方を少し変えるとわかりやすくなります。普通の規則。同値変形してこうする。要するに「代入後の x の値を x' とすれば A[x'/x] である」が事前条件です。Hoare triple の意味を考…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。