7.2A programkonstrukciók programfüggvénye

7.2A programkonstrukciók programfüggvénye
Előző	7. fejezet - Programkonstrukciók	Következő

Miután beláttuk, hogy meglevő programokból a programkonstrukciók segítségével új programokat készíthetünk, vizsgáljuk meg, hogy milyen kapcsolat van a konstruált programok programfüggvénye és az eredeti programok programfüggvénye között.

A szekvencia a legegyszerűbb programkonstrukció, ennek megfelelően a programfüggvénye is egyszerűen felírható a két komponensprogram programfüggvényének segítségével. Mivel a szekvencia két program egymás utáni elvégzését jelenti, várható, hogy a programfüggvénye a két komponensprogram programfüggvényének kompozíciója. Azonban mint látni fogjuk kompozíció helyett szigorú kompozíciót kell alkalmazni.

7.2. TéTEL: A SZEKVENCIA PROGRAMFüGGVéNYE Legyen tetszőleges állapottér, programok -n, . Ekkor

Bizonyítás: Legyen tetszőleges. Ekkor

tehát:

Legyen . Ekkor

Vegyük észre, hogy a nem szigorú kompozíció értelmezési tartományában olyan pont is lehet, amelyhez a szekvencia rendel végtelen sorozatot is. Nézzünk erre egy egyszerű példát: Legyen ,

Ekkor , de .

Mivel az elágazást több programból képezzük, a programfüggvényét is csak kissé körülményesebben tudjuk megfogalmazni. Hiszen az, hogy egy ponthoz az elágazás rendel-e végtelen sorozatot attól is függ, hogy mely feltételek igazak az adott pontban. Sőt, ha egy pontban egyetlen feltétel sem igaz, akkor a komponensprogramok programfüggvényétől függetlenül abban a pontban az elágazás programfüggvénye nem lesz értelmezve. Az elágazás programfüggvényének formális megfogalmazását adja meg a következő tétel.

7.3. TéTEL: AZ ELáGAZáS PROGRAMFüGGVéNYE Legyen tetszőleges állapottér, programok, valamint feltételek -n, . Ekkor

:
ahol

Bizonyítás: Legyen tetszőleges. Ekkor

Legyen továbbá . Ekkor

Természetesen, ha az elágazás-feltételek lefedik az egész állapotteret, akkor az a feltétel, hogy valamelyik -nek igaznak kell lennie, triviálisan teljesül.