Ebben az alfejezetben megvizsgáljuk a programkonstrukciók és a specifikáció kapcsolatát.

Először azt fogjuk megvizsgálni, hogy a szekvencia adott utófeltételhez tartozó leggyengébb előfeltétele milyen kapcsolatban van az őt alkotó programok leggyengébb előfeltételével.

7.5. TéTEL: A SZEKVENCIA LEVEZETéSI SZABáLYA Legyen , és adott , és állítás -n. Ha

akkor .

Bizonyítás: Legyen . Ekkor (1) miatt és . Mivel (2) miatt : .

Továbbá (2) miatt , tehát .

_

A szekvencia levezetési szabálya és a specifikáció tétele alapján a következőt mondhatjuk: ha és olyan programok, amelyekre a paramétertér minden pontjában és teljesül, akkor megoldja a párokkal adott feladatot.

7.6. TéTEL: A SZEKVENCIA LEVEZETéSI SZABáLYáNAK MEGFORDíTáSA Legyen , és , olyan állítások -n, amelyekre . Ekkor állítás, amire

Bizonyítás: Legyen . Ekkor (2) automatikusan teljesül. Csak (1) fennállását kell belátnunk. Ehhez indirekt feltesszük, hogy

Ez kétféleképpen fordulhat elő:

_

Vizsgáljuk meg, mi a kapcsolat az elágazás és az őt alkotó programok adott utófeltételhez tartozó leggyengébb előfeltétele között.

7.7. TéTEL: AZ ELáGAZáS LEVEZETéSI SZABáLYA Legyen , és adott , állítás -n. Ha

akkor

Bizonyítás: Legyen , és tegyük fel, hogy valamelyik feltétel igaz -ra, azaz . Ekkor , ui.

Másrészt mivel :

azaz .

_

Felhasználva a specifikáció tételét és az elágazás levezetési szabályát azt mondhatjuk: Legyen adott az feladat specifikációja ( ). Ekkor ha minden paraméterre és minden programra , és minden paraméterhez van olyan feltétel, amelyre , akkor az elágazás megoldja a párokkal specifikált feladatot.

Hasonlóan a szekvencia levezetési szabályához az elágazás levezetési szabálya is megfordítható, tehát ha egy elágazás megold egy specifikált feladatot, akkor le is lehet vezetni.

7.8. TéTEL: AZ ELáGAZáS LEVEZETéSI SZABáLYáNAK MEGFORDíTáSA Legyen , és , olyan állítások -n, amelyekre

Ekkor

Bizonyítás: Indirekt: tegyük fel, hogy

Legyen . Ekkor két eset lehetséges:

_

Természetesen nem elég az elágazás levezetési szabályának teljesülését vizsgálni, ha arra vagyunk kíváncsiak, hogy az elágazás megold-e egy feladatot. Soha nem szabad elfeledkeznünk arról, hogy leellenőrizzük, hogy a feltételek lefedik-e a feladat értelmezési tartományát.

Ha , akkor a levezetési szabály teljesülése – a specifikáció tétele alapján – garantálja, hogy az elágazás megoldja a feladatot.

Az előző két konstrukcióhoz hasonlóan most megvizsgáljuk, hogy milyen kapcsolat van a ciklus és a ciklusmag leggyengébb előfeltétele között.

7.9. TéTEL: A CIKLUS LEVEZETéSI SZABáLYA Adott , , állítás -n, függvény és legyen . Ha

akkor

Jelölje a továbbiakban a ciklusmag programfüggvényének a ciklusfeltételre vonatkozó leszűkítését, azaz . Mielőtt magát a levezetési szabályt bizonyítanánk, ennek a relációnak látjuk be két tulajdonságát:

7. állítás: Legyen . Ekkor

Bizonyítás:  szerinti teljes indukcióval:

_

2. állítás: Legyen . Ekkor

Bizonyítás: Indirekt: tegyük fel, hogy . Tekintsünk egy tetszőleges pontot. Ekkor , ugyanis (5)-ben helyére -t írva: teljesül. Ekkor viszont

azaz

Ez viszont ellentmond (3)-nak.

_

Bizonyítás: (Ciklus levezetési szabálya) Legyen tetszőleges. Mivel (1) miatt , ezért vagy teljesül.

_

A levezetési szabályban szereplő állítást a ciklus invariáns tulajdonságának, a függvényt terminálófüggvénynek nevezzük. A invarianciáját az (1) és (4) feltételek biztosítják: garantálják, hogy az invariáns tulajdonság a ciklusmag minden lefutása előtt és után teljesül. A terminálófüggvény a ciklus befejeződését biztosítja: az (5) pont alapján a ciklusmag minden lefutása legalább eggyel csökkenti a terminálófüggvényt, másrészt a (3) miatt a terminálófüggvénynek pozitívnak kell lennie. A (2) feltétel garantálja, hogy ha a ciklus befejeződik, akkor az utófeltétel igazsághalmazába jut.

A ciklus levezetési szabályának és a specifikáció tételének felhasználásával elégséges feltételt adhatunk a megoldásra: ha adott a feladat specifikációja ( ), és találunk olyan invariáns állítást és terminálófüggvényt, hogy a paramétertér minden elemére teljesül a ciklus levezetési szabályának öt feltétele, akkor a ciklus megoldja a párokkal definiált feladatot.

A ciklus levezetési szabálya visszafelé nem igaz, azaz van olyan ciklus, amit nem lehet levezetni. Ennek az az oka, hogy egy levezetett ciklus programfüggvénye mindig korlátos lezárt, hiszen az állapottér minden pontjában a terminálófüggvény értéke korlátozza a ciklusmag lefutásainak számát.

Az is könnyen látható, hogy ha a ciklus programfüggvénye nem korlátos lezárt, akkor nem tudunk a ciklushoz terminálófüggvényt adni. Ám ha egy ciklus programfüggvénye megegyezik a ciklusmag ciklusfeltételre vonatkozó korlátos lezártjával, akkor a ciklus levezethető.

7.10. TéTEL: A CIKLUS LEVEZETéSI SZABáLYáNAK MEGFORDíTáSA Legyen , és , olyan állítások -n, amelyekre , és tegyük fel, hogy . Ekkor létezik állítás és függvény, amelyekre

Bizonyítás: Legyen és válasszuk -t úgy, hogy :

Ekkor

_

Azt, hogy a lezárt és a korlátos lezárt megegyezik, a definíciójában használtuk ki: ez a feltétel garantálja, hogy a definícióban szereplő maximum véges.