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.
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).
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.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.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.12. Definíció (Reláció ősképe).
a
halmaz
relációra vonatkozó ősképe [[???WRMP 95]].
1.14. Definíció (Relációk szigorú kompozíciója).
az
és az
relációk szigorú kompozíciója [[???Hor 90]].
Haladási tulajdonságok megfogalmazásához szükségünk lesz relációk tranzitív diszjunktív lezártjának fogalmára.
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.
Jelöljük -rel azon változók halmazát, amelyektől az
reláció függ.
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.
.