Poprawno±¢ i peªno±¢ systemu Hoare'a

Poprawno±¢ i peªno±¢ systemu Hoare'a

Wprowad¹my dwie instrukcje o nast¦puj¡cej semantyce.

Denicja

nww(skip, p) = p, nww(abort, p) = false.

Ponadto Denicja

W = while B do S

W⁰=if B then abort else skip W^k+1=if B then S;W^kelse skip

To jest inny zapis p¦tli. W szczególno±ci wykonanie pewnego W^k poci¡ga W.

Lemat

nww(W⁰,p) ≡ ¬B ∧ (¬B ⇒ p).

Dowód

nww(W⁰,p) =

nww(W⁰=if B then abort else skip, p) = (B ⇒ nww(abort, p)) ∧ (¬B ⇒ nww(skip, p)) ≡

(B ⇒ false) ∧ (¬B ⇒ p) ≡

(¬B ∨ false) ∧ (¬B ⇒ p) ≡

¬B ∧ (¬B ⇒ p)

Lemat W∞

k=0nww(W^k,p) → nww(W, p) Dowód jest indukcyjny.

Dla k = 0 mamy:

nww(W⁰,p) → ¬B ∧ (¬B ⇒ p) nww(W⁰,p) → ¬B ∧ p

nww(W⁰,p) → (¬B ∧ p) ∨ (B ∧ nww(S ; W,p)) nww(W⁰,p) → nww(W, p)

Dla k > 0:

nww(W^k+1,p) = nww(ifBthen S ; W^kelse skip , p)

nww(W^k+1,p) ≡ (B → nww(S ; W^k,p)) ∧ (¬B → nww(skip, p)) nww(W^k+1,p) ≡ (B → nww(S, nww(W^k,p)) ∧ (¬B → nww(skip, p)) nww(W^k+1,p) ≡ (B → nww(S, nww(W^k,p)) ∧ (¬B → p)

nww(W^k+1,p) → (B → nww(S, nww(W, p)) ∧ (¬B → p) nww(W^k+1,p) → (B → nww(S ; W, p)) ∧ (¬B → p) nww(W^k+1,p) → nww(W, p)

Twierdzenie

Je±li ` {p}S{q}, to |= {p}S{q}.

Dowód jest indukcyjny ze wzgl¦du na dªugo±¢ dowodu w systemie Hoare'a. Dziedzina nas nie interesuje, bo przykªadowo wªasno±ci liczb naturalnych s¡ prawdziwe. Poprawno±¢ reguªy konsekwencji wynika z poprawno±ci Modus ponens. Ponadto, |= {p}S{q} wtw, gdy |= p → nww(S, q). Mo»na zaj¡¢ si¦ |= p → nww(S, q).

Oczywi±cie aksjomat przypisania jest poprawny. Zajmijmy si¦

zªo»eniem S1 ; S2 i zaªo»eniem indukcyjnym |= p → nww(S1, q) oraz |= q → nww(S2, r). Z drugiego i monotoniczno±ci mamy:

|=nww(S1, q) → nww(S1, nww(S2, r)) Wtedy

|=p → nww(S1, nww(S2, r))

i mamy tez¦ po zªo»eniu S1 i S2 Dowód dla p¦tli i instrukcji warunkowej prowadzimy podobnie.

Twierdzenie

Je±li |= {p}S{q}, to ` {p}S{q}.

Dowód dla p¦tli W = while B do S.

|=nww(W, q) ∧ B → nww(S ; W, q)

|=nww(W, q) ∧ B → nww(S, nww(W, q))

` {nww(W, q) ∧ B}S{nww(W, q)}

` {nww(W, q)}W{nww(W, q) ∧ ¬B}

` (nww(W, q) ∧ ¬B) → q

` {nww(W, q)}W{q}

`p → nww(W, q)

` {p}W{q}