わりとわかりにくくて混乱しやすい気がするホーア論理の代入の規則ですが，見方を少し変えるとわかりやすくなります。普通の規則。同値変形してこうする。要するに「代入後の x の値を x' とすれば A[x'/x] である」が事前条件です。Hoare triple の意味を考…