3. fejezet - Specifikáció
Előző I. rész - Bevezetés a programozáshoz (Fóthi Ákos) Következő

3. fejezet - Specifikáció

Tartalom

3.1A leggyengébb előfeltétel
3.2A feladat specifikációja
3.3A változó fogalma
3.4Példák
3.5Feladatok

A megoldás definíciója közvetlenül elég nehézkesen használható a programok készítése során, hiszen az, hogy egy program megold-e egy feladatot az a megoldás eddigi definíciója alapján csak nehezen ellenőrizhető. Ezért bevezetünk néhány új fogalmat, majd ezek segítségével megadjuk a megoldás egy elégséges feltételét.

3.1A leggyengébb előfeltétel

Először a program működésének eredményét adjuk meg egy a programfüggvénynél kényelmesebben használható jellemzővel.

3.1. Definíció (LEGGYENGéBB ELőFELTéTEL).

Legyen program, állítás. Ekkor az program utófeltételhez tartozó leggyengébb előfeltétele az a , függvény amelyre:

A leggyengébb előfeltétel tehát pontosan azokban a pontokban igaz, ahonnét kiindulva az program biztosan terminál, és az összes lehetséges végállapotra igaz .

Természetesen a leggyengébb előfeltétel igazsághalmazán kívül is lehetnek olyan pontok, amelyből a program egy futása eljut az utófeltétel igazsághalmazába, csak azokból a pontokból nem garantált, hogy oda jut.

Egy program működése úgy is jellemezhető, hogy megadjuk a program tetszőleges utófeltételhez tartozó leggyengébb előfeltételét. A feladat megoldása során az a célunk, hogy olyan programot találjunk, amelyik bizonyos feltételeknek eleget tevő pontokban terminál. Ezért azt mondhatjuk, hogy ha a számunkra kedvező végállapotokra megadjuk a program leggyengébb előfeltételét, akkor a programfüggvény meghatározása nélkül jellemezzük a program működését.

Emlékeztetünk arra, definiáltuk a reláció szerinti őskép fogalmát is, ennek felhasználásával azonnal látszik, hogy

Felhasználva az igazsághalmaz definícióját és a szigorú kompozíció szerinti őskép tulajdonságát

Mivel függvény, a kompozíció és a szigorú kompozíció megegyezik, tehát

Abban az esetben, ha is függvény .

A fenti összefüggésekre gyakran fogunk hivatkozni.

A most következő tétel a leggyengébb előfeltétel néhány nevezetes tulajdonságáról szól.

3.1. TéTEL: A TULAJDONSáGAI Legyen program, állítások. Ekkor

  1. ,

  2. Ha , akkor ,

  3. ,

  4. .

Az első tulajdonságot a csoda kizárása elvének, a másodikat monotonitási tulajdonságnak nevezzük.

Bizonyítás: 

  1. Indirekt: Tegyük fel, hogy . Ekkor a leggyengébb előfeltétel definíciója szerint: és . Ez nyilvánvaló ellentmondás.

  2. Indirekt: Tegyük fel, hogy . Ekkor és . Ez viszont ellentmond annak a feltételnek, mely szerint

  3. Az állítást két részben, a mindkét irányú következés belátásával bizonyítjuk.

    1. , ugyanis:

      Legyen . Ekkor és , azaz és , illetve . Ekkor azonban , azaz .

    2. , ui.:

      Legyen . Ekkor a leggyengébb előfeltétel definíciója alapján és . Felhasználva, hogy , adódik, hogy és , azaz és , tehát .

  4. Legyen . Ekkor vagy . Ha , akkor – a monotonitási tulajdonság alapján – . Hasonlóan ha , akkor .

A tulajdonságoság visszafelé nem igaz. nem következik sem , sem . Természetesen, ha determinisztikus, azaz legfeljebb egy elemű halmaz, akkor az egyenlőség fennáll.

Előző Fel Következő
2.8Feladatok Tartalom 3.2A feladat specifikációja