23.2.Haladási feltételek finomítása

23.2.Haladási feltételek finomítása
Előző	23. fejezet - Levezetési szabályok	Következő

23.2. Lemma.
( finomítása) megfelel a specifikációs feltételnek, ha az alábbi szabályok alkalmazásával levezethető:

Ha megfelel -nak, akkor megfelel -nak is.
Tranzitivitás: ha megfelel -nak és megfelel -nak, akkor megfelel -nak is.
Diszjunkció: bármely W megszámlálható halmazra: ha megfelel -nak, akkor megfelel -nak is.

Biz.: . def. és a .,. tételek felhasználásával: (1) A feltétel szerint . Ekkor . def. szerint . (2)-es és (3)-as esetben hasonlóan.

23.3. Lemma.
( feltétel bizonyítása) Az program pontosan akkor felel meg a specifikációnak, ha megfelel a feltételnek, tehát biztosan fixpontba jut.

Biz.: A . lemma szerint , így a . lemma felhasználásával: megfelel a feltételnek.

23.1. Definíció (Variáns függvény).
Variáns függvénynek nevezzük a , az állapotokhoz egészeket rendelő függvényeket. Legyen tetszőleges egész szám. A logikai függvényeket definiáljuk az igazsághalmazukkal: , .

A következő tételben a UNITY indukciós elvét [[???Cha Mis 89]] fogalmazzuk meg a ciklus levezetési szabályához hasonló alakban [[???Fót 83, ???WRMP 95]].

23.4. Tétel.
(Variánsfüggvény alkalmazása) Legyen logikai függvény és egy olyan variáns függvény, amelyre teljesül, hogy . Ha , akkor .

Biz.: Teljes indukcióval belátjuk, hogy . Ebből a . def. alapján, a diszjunktivitás felhasználásával , azaz adódik. A feltétel szerint , így . Tehát . A . lemma szerint . A . def., a diszjunktivitás alkalmazásával: . Teljes indukció: Alapeset: . A tétel feltétele szerint: . Tudjuk, hogy , így . Indukciós feltevés: . A . def. alapján, a diszjunktivitás felhasználásával: . A . lemma alapján: . A diszjunkció ismételt alkalmazásával: . A tétel feltétele szerint: . , így . Tehát . A . def. szerint, a tranzitivitás alkalmazásával: .

23.5. Tétel.
( finomítása variánsfüggvény alkalmazásával) Legyen logikai függvény és egy olyan variáns függvény, amelyre teljesül, hogy . Ha megfelel a specifikációs feltételnek, akkor megfelel a specifikációs feltételnek is.

Biz.: Az előző tétel (.) bizonyítása alapján a bizonyítás megkonstruálható. A bizonyítás során a . def. helyett a . lemmára kell hivatkozni. A . lemma helyett pedig a lemma azon következményére van szükség, amely szerint tetszőleges program megfelel a feltételnek.

23.6. Lemma.
Legyen , válasszunk egy olyan variáns függvényt, amelyre: . Ha minden -re , akkor megfelel tetszőleges logikai függvény esetén a specifikációs feltételnek (pl. a specifikációs feltételnek is).

Biz.: A feltétel és a . tétel szerint: . A . tétel alapján bármely logikai függvénnyel szűkíthetjük baloldalát: . A . def. alapján , ill. választás mellett megfelel a , specifikációs feltételeknek.

Legyen . Ha választunk egy olyan variáns függvényt, amelyre , akkor miatt: . Ha minden -re , akkor megfelel a tetszőleges logikai függvény esetén a specifikációs feltételnek a tétel szerint. A . tétel szerint éppen a program által elérhető állapotok halmaza. Ezért megfogalmazhatjuk az alábbi tételt:

23.7. Tétel.
(Biztosan fixpontba jut) Legyen . Válasszunk egy olyan variáns függvényt, amelyre . Ha megfelel a specifikációs feltételnek minden -re, akkor megfelel a specifikációs feltételnek is, azaz biztosan fixontba jut.

23.1. Megjegyzés.
A . tétel nem használható feladatok finomítására, mert csak akkor alkalmazható, ha a állítás ismert, azaz a program adott. A . tétel helyességbizonyítási eszköz.

23.8. Tétel.
(A fixpontfeltétel finomítása) Ha megfelel a , specifikációs feltételeknek és , akkor megfelel a specifikációs feltételnek is.

Biz.: A . és a . lemma alapján elegendő megmutatni, hogy megfelel a feltételnek. A feltétel és a . lemma szerint van olyan invariáns, hogy és . . lemma szerint ekkor . Így található olyan invariáns, hogy és . A . lemma alapján ezzel beláttuk, hogy megfelel a feltételnek.