Ebben a fejezetben bevezetünk néhány egyszerű programot. Ezeket a programokat a következő fejezetekben gyakorta fogjuk használni, ezért megvizsgáljuk a programfüggvényüket, és egy adott utófeltételhez tartozó leggyengébb előfeltételüket.

Az elemi programok közül is kiválasztunk néhány speciális tulajdonsággal rendelkezőt, és a továbbiakban csak velük foglalkozunk.

Az első ilyen program, az üres program lesz, ami nem csinál semmit.

A második program a törlődés, aminek legfontosabb jellemzője, hogy soha sem terminál.

Az eddig felsorolt két elemi program segítségével még bajosan tudnánk egy adott feladatot megoldó programot készíteni, hiszen egyrészt nem túl sok olyan feladat van, aminek az program megoldása lenne (vajon van ilyen egyáltalán?) és a program is csak egy nagyon szűk feladatosztálynak lehet megoldása (melyek ezek a feladatok?). A harmadik – és a programozási feladat megoldása szempontjából legfontosabb – speciális elemi program az értékadás.

A definíció alapján könnyen látható, hogy az relációra fennáll az alábbi tulajdonság:

A fenti komponensrelációk tehát pontosan azt írják le, hogy az adott értékadás miként változtatja meg az állapottér egyes komponenseit.

Ha egy kivételével az összes projekció – azaz az értékadás az állapottérnek csak egy komponensét (csak egy változó értékét) változtatja meg –, akkor -et egyszerű értékadásnak, egyébként szimultán értékadásnak nevezzük.

Az értékadás egy kicsit bonyolultabb mint előző két társa, de egy kicsit „értékesebb" is, hiszen értékadással minden feladat megoldható! A kérdés persze csupán az, hogy az éppen adott feladat által definiált értékadás megengedett művelet-e. Ezzel a kérdéssel a későbbiekben – a programozási feladat megoldása során – fogunk foglalkozni.

Vizsgáljuk meg a fent definiált speciális elemi programok programfüggvényeit! 6.1. TéTEL: ELEMI PROGRAMOK PROGRAMFüGGVéNYE

A tételt bizonyítása triviális, ezért itt nem bizonyítjuk (a feladatok között szerepel).

Most, hogy megvizsgáltuk a programfüggvényeket, nézzük meg az elemi programok adott utófeltételhez tartozó leggyengébb előfeltételét.

Mivel a SKIP program programfüggvénye az identikus leképezés, egy tetszőleges utófeltételhez tartozó leggyengébb előfeltétele:

Hasonlóan egyszerűen látható, hogy – mivel az program programfüggvénye üres – a leggyengébb előfeltétel definíciója alapján egy teszőleges utófeltétel esetén

Az általános értékadás leggyengébb előfeltételét külön vizsgáljuk a determinisztikus és nem determinisztikus, illetve a globális, és a parciális esetben.

Legyen függvény. Ekkor

Ha parciális függvény, akkor az általa definiált értékadás is parciális, melynek leggyengébb előfeltétele:

Most vizsgáljuk azt a két esetet, amikor nem determinisztikus. Feltéve, hogy , az értékkiválasztás leggyengébb előfeltétele

Ugyanez parciális esetben:

Az értékadást általában változókkal írjuk le. Legyenek az állapottér változói rendre . Ekkor az program jelölésére az alábbi formulát használhatjuk.

A gyakorlatban az esetek többségében komponenseinek nagy része projekció, azaz Ekkor az értékadás jelöléséből a bal oldalról -t , a jobb oldalról pedig -t elhagyjuk. Vegyük észre, hogy egyszerű értékadás esetén a bal oldalon csak egy változó, a jobb oldalon pedig csak egy kifejezés marad.

Jelölésünket abban az esetben még tovább egyszerűsíthetjük, ha az értékadás jobb oldala ( ) nem függ minden változótól. Ekkor a jobb oldalon csak azokat a változókat tüntetjük fel, amelyektől függ.

Nézzük meg egy egyszerű példán a fent leírtakat: Legyen az állapottér

A továbbiakban a fentihez hasonlóan az állapottér egyes komponenseihez tartozó változókat a komponensek alá fogjuk írni. Legyenek az értékadás komponensei: :

Ekkor az értékadás változókkal felírva:

A jelölés fent leírt egyszerűsítéseit elvégezve az

egyszerű értékadást kapjuk.

Ha felhasználjuk, hogy az értékadás leggyengébb előfeltétele , akkor egy változókkal felírt értékadás változókkal megadott előfeltételét egyszerűen kiszámíthatjuk: helyettesítsük az utófeltételben az értékadásban szereplő változókat az új értékükkel. Erre bevezetünk egy új jelölést is: legyenek rendre az állapottér változói. Ekkor