ホーア論理の代入の規則

わりとわかりにくくて混乱しやすい気がするホーア論理の代入の規則ですが，見方を少し変えるとわかりやすくなります。

普通の規則。

\{A[e/x]\} \mathtt{x := e} \{A\}

同値変形してこうする。

\{\forall x'. x' = e \to A[x'/x]\} \mathtt{x := e} \{A\}

要するに「代入後の x の値を x' とすれば A[x'/x] である」が事前条件です。Hoare triple の意味を考えればそれが事前条件になるのは当たり前ですね。

こっちのほうがわかりやすいし，この形で認識しておくと x' の条件を変えることでいろいろできます。例えば乱数。

\{\forall x'. A[x'/x]\} \mathtt{x := rand()} \{A\}

上限を指定したり。

\{\forall x'. 0 \le x' < n \to A[x'/x]\} \mathtt{x := rand(n)} \{A\}

配列。

\{\forall x'. x'[i] = e \to (\forall j. i \ne j \to x'[j] = x[j]) \to A[x'/x]\} \mathtt{x[i] := e} \{A\}

配列への同時代入（構文は適当）。

\small\{\forall x'. (\forall j. 0 \le j \le 3 \to x'[i+j] = y[k+j]) \land (\forall j. \neg(i \le j \le i+3) \to x'[j] = x[j]) \to A[x'/x]\} \mathtt{x[i:i+3] := y[k:k+3]} \{A\}