19.3.A relációs modell alapfogalmai

A feladat és az absztrakt program pontos jelentését úgy adhatjuk meg, hogy a feladat specifikációjában szereplő kikötésekhez, ill. az absztrakt programot leíró utasításhalmazhoz relációt rendelünk hozzá. A feladatot, ill. a programot leíró relációkat az állapottér, az állapottér hatványhalmaza, és ezek direkt szorzatai felett értelmezzünk. Az alapfogalmak definíciói megegyeznek a könyv első részében adottakkal.

Az állapottér véges sok legfeljebb megszámlálhatóan végtelen típusértékhalmaz direkt szorzata [[???Fót 83]].

19.1. Definíció (Állapottér).

megszámlálható halmaz. Az halmazt állapottérnek, az halmazokat típusértékhalmazoknak nevezzük.

19.2. Definíció (Állapot).

Az állapottér elemeit, az pontokat állapotoknak nevezzük.

A feladat matematikai megfogalmazásához szükségünk lesz a reláció és a sorozat fogalmára. Megismételjük a reláció, bináris reláció és a reláció értelmezési tartománya definícióját (. fejezet).

19.3. Definíció (Reláció).

Az halmazt relációnak Példa: , . . . nevezzük.

Az -t bináris relációnak nevezzük.

19.4. Definíció (Reláció értéke).

halmaz az reláció értéke A példa relációjának képe az pontban: . az pontban.

19.5. Definíció (Reláció értelmezési tartománya).

Az reláció értelmezési tartománya: A példa relációjának értelmezési tartománya: .

Jelölések:

véges sorozat:

végtelen sorozat:

: elemeiből képzett véges sorozatok halmaza

: elemeiből képzett végtelen sorozatok halmaza

A feladat matematikai megfelelője feltételek együttese. A specifikációs feltételek megfogalmazásához logikai függvényeket használunk. Logikai függvényeket igazsághalmazukkal, egy alaphalmaz adott részhalmazával jellemezhetjük. A specifikációs relációk leírásához szükségünk lesz a hatványhalmaz fogalmára. Minden egyes specifikációs feltétel az állapottér hatványhalmaza felett értelmezett reláció.

1.6. Definíció (Hatványhalmaz).

Az halmaz részhalmazainak halmazát az hatványhalmazának nevezzük és -val jelöljük.

A feladat matematikai megfelelője feltételek együttese. Minden egyes feltétel az állapottér hatványhalmaza felett értelmezett reláció. Az állapottér részhalmazait logikai relációkkal jellemezzük. Megadjuk a logikai reláció, logikai függvény és igazsághalmazuk definícióját.

1.7. Definíció (Parciális függvény).

Az reláció determinisztikus reláció, (vagy parciális függvény), ha Parciális függvények esetén az jelölést alkalmazzuk.

1.8. Definíció (Függvény).

Az reláció függvény, ha Függvények esetén az jelölést használjuk.

1.9. Definíció (Logikai függvény, logikai reláció).

reláció logikai reláció , ahol a logikai értékek halmaza. Logikai függvény-ről beszélünk, ha a logikai reláció függvény.

Jelölés: - az azonosan igaz, - az azonosan hamis logikai függvény.

1.10. Definíció (Logikai függvény igazsághalmaza).

az logikai függvény (állítás) igazsághalmaza Példa: . . . . .

1.1. Megjegyzés (Logikai műveletek).

A logikai relációk felett értelmezzük a műveleteket, oly módon, hogy azok megfeleljenek a relációk igazsághalmazaira vonatkozó halmazműveleteknek. Azaz: , , , , és . A jeleket bizonyítások szövegének rövidítésére használjuk, a „ha, akkor”, „akkor és csak akkor”, ill. „akkor, ha” állítások leírásának rövidítésére.

1.11. Definíció (Reláció inverz képe).

a halmaz relációra vonatkozó inverz képe.

1.12. Definíció (Reláció ősképe).

a halmaz relációra vonatkozó ősképe [[???WRMP 95]].

1.13. Definíció (Relációk kompozíciója).

az és az relációk kompozicíója.

1.14. Definíció (Relációk szigorú kompozíciója).

az és az relációk szigorú kompozíciója [[???Hor 90]].

1.15. Definíció (Reláció igazsághalmaza).

az reláció igazsághalmaza.

Haladási tulajdonságok megfogalmazásához szükségünk lesz relációk tranzitív diszjunktív lezártjának fogalmára.

1.16. Definíció (Reláció tranzitív diszjunktív lezártja).

reláció az reláció tranzitív diszjunktív lezártja, ha a legkisebb olyan reláció, amelyre: , ha és , akkor és bármely megszámlálható halmazra: .

1.1. Példa (Reláció tranzitív diszjunktív lezártja).

, , ,

1.17. Definíció ( ).

Legyen . annak az állításnak a rövid megfogalmazása, hogy az reláció igazsághalmaza megegyezik -val [[???Dij Sch 89]].

1.2. Megjegyzés.

.

1.18. Definíció (Változó).

A projekciókat változóknak nevezzük. A fenti definíció szerint a változó tehát nem szintaktikus fogalom. A továbbiakban amíg a választott programozási modell keretein belül maradunk nem vizsgáljuk formális nyelvek és szemantikai tartományok lehetséges kapcsolatrendszereit. Ha szükséges, a későbbiek során könnyen definiálható formális nyelv és szemantikus leképezés. A szemantikai tartomány elemei az általunk megfogalmazott modellben definiált egyes matematikai objektumok lehetnek. A változók megadásakor a projekció értelmezési tartományát, az állapotteret, általában elhagyjuk: .

1.19. Definíció (Vetítés altérre).

Legyen az direkt szorzat altere. függvény az -beli pontokhoz az -beli vetületüket rendeli. A függvényt általánosítjuk részhalmazaira, -beli elemek sorozataira, felett értelmezett bináris relációkra oly módon, hogy a részhalmazok és sorozatok elemeit ill. a relációk elemeinek komponenseit pontonként vetítjük az altérre [[???WRMP 95]].

Értékadások vizsgálatánál gyakran van arra szükség, hogy meghatározzuk milyen változók kaphatnak új értéket, illetve milyen változók értékétől függ az eredmény. Értékadást hatásrelációja jellemez, így a értékadások vizsgálata a hatásrelációjuk vizsgálatára vezethető vissza.

1.20. Definíció (Reláció független egy változótól).

Legyen és . Azt mondjuk, hogy az reláció független az komponenstől és a változótól, ha

Jelöljük -rel azon változók halmazát, amelyektől az reláció függ.

1.21. Definíció (Reláció nem változtatja meg).

Legyen és . Azt mondjuk, hogy az reláció nem változtatja meg az komponens és a változó értékét, ha .

Jelöljük -rel azon változók halmazát, amelyeket az reláció megváltoztat. .