ALAPFOGALMAK 1. A reláció az program programfüggvénye, ha. Azt mondjuk, hogy az feladat szigorúbb, mint az feladat, ha

ALAPFOGALMAK

1

Állapottér Legyen I egy véges halmaz és legyenek Ai, iI tetszőleges véges vagy megszámlálható, nem üres halmazok. Ai halmazt állapottérnek, az Ai halmazokat pedig típusértékhalmazoknak nevezzük

Ekkor az A= A feladat

Az állapottér segítségével megfogalmazzuk, hogy egy adott állapotból ( azaz az állapottér egy eleméből, pontjából) milyen állapotba (azaz az állapottér mely pontjába) akarunk eljutni. Feladatnak nevezzük egy

relációt.

A program Programnak nevezzük az 1.

relációt, ha

,

2.

,

3.

.

A programfüggvény reláció az

A

program programfüggvénye, ha

1.

,

2.

.

Megoldás Azt mondjuk, hogy az S program megoldja az F feladatot, ha 1.

,

a

2.

. A

A

Szigorítás feladat szigorúbb, mint az

Azt mondjuk, hogy az 1. 2.

, .

Programozás módszertan 1. vizsga

feladat, ha

KITERJESZTÉS

2

A feladat kiterjesztése Legyen a B állapottér altere az A állapottérnek. Az

relációt az

kiterjesztésének nevezzük, ha

feladat .

Program kiterjesztése Legyen a B állapottér altere A állapottérnek, és jelölje S program a B állapottéren. Ekkor az

a B kiegészítő alterét A-ra. Legyen továbbá

A-beli relációt az S program kiterjesztésének nevezzük, ha .

Kiterjesztési tételek Bővített identitás a B kiegészítő altere A-ra,

Legyen B altere A-nak

reláció. A G bővített identitás

és

felett, ha

és

.

Vetítéstartás feladat. A G vetítéstartó B felett, ha

Legyen B altere A-nak,

. Félkiterjesztés Legyen B altere A-nak,

feladat,

. Azt mondjuk, hogy a G félkiterjesztés H felett, ha

. Kiterjesztés tételek Legyen B altere A-nak, a

a B kiegészítő altere A-ra, S program B-n.

S-nek, illetve F-nek kiterjesztése A-ra. Legyen továbbá ,

feladat,

olyan feladat, melyre

pedig olyan program, amely ekvivalens S-sel B-n.

Ekkor az alábbi állítások teljesülnek: 1. ha

megoldása

2. ha

megoldása -nek , akkor S megoldása F-nek;

3. ha

megoldása

-nek , akkor S megoldása F-nek;

-nek , akkor S megoldása F-nek;

4. a.) ha

megoldása -nek, és

b.) ha

megoldása -nek, és

5. ha S megoldása F-nek, akkor

vetítéstartó B felett, akkor S megoldása F-nek; félkiterjesztés megoldása

felett, akkor S megoldása F-nek; -nek;


illetve

KITERJESZTÉS

3

6. ha s megoldása F-nek, és

bővített identitás

felett és vetítéstartó B felett, akkor

megoldása -nek; 7. ha S megoldása F-nek, és

félkiterjesztés

felett, akkor

megoldása

-nek.

*Bizonyítás A 4. tételből következik az első három, hiszen , és

félkiterjesztés

4. tétel bizonyítása: Legyen

ekvivalens S-sel B-n, és

vetítétartó, illetve

-en. tetszőleges. Ekkor megoldás

tehát

, így a megoldás első kritériumának teljesülését bebizonyítottuk. Tekintsük most a

második kritériumot; legyen

Az a. esetben, azaz

tetszőlegesen rögzített. Ekkor

vetítéstartó, akkor

-ra .

Ekkor tetszőleges

esetén, mivel a megoldás definíciója miatt

,

. Tehát a megoldás második feltételek is teljesül. A b. esetben, azaz ha

félkiterjesztés, akkor

, azaz

a megoldás definíciója miatt

, tehát

, és ezzel ebben az esetben is beláttuk, hogy az S program megoldja F feladatot.


, és

MEGOLDÁS

4

Megoldás átnevezéssel Legyen

feladat és

,

program. Azt mondjuk, hogy S az

átnevezéssel

megoldása F-nek, ha 1. 2.

.

Az általánosított megoldás Legyen ,

feladat és

program. Ha létezik olyan C és D állapottér, hogy

,

A altere C-nek, B altere D-nek, és S kiterjesztése D-re átnevezéssel megoldása F C-re való kiterjesztettjének, akkor azt mondjuk, hogy S – általános értelemben – megoldása F-nek. Reláció szerinti megoldás Legyen A és B tetszőleges állapottér,

program és

,

. Azt mondjuk,

hogy S szerint megoldása F-nek, ha , és

1. 2.

.

A kompozíció és a szigorú kompozíció megegyezik, ha legalább az egyik reláció függvény, ezért a megoldás átnevezéssel a reláció szerinti megoldás speciális esete.Így a következő tétel arra is alkalmazható. Reláció szerinti megoldás tétele Legyen F tetszőleges feladat, az állapottere A, egy paramétere B, elő –és utófeltétele pedig Legyen

program és

tetszőleges olyan reláció, melyre

, . , akkor az S program

szerint megoldja az F feladatot.

*Bizonyítás A 1.

szerinti megoldás definíciója két pontjának teljesülését kell belátnunk. . Programozás módszertan 1. vizsga

.

. Definiáljuk a

következő függvényeket:

Ekkor, ha

és

MEGOLDÁS Legyen

5 . Ekkor

. Mivel

,

és Felhasználva, hogy

.

: és

Mivel

.

,

,

tehát

.

2.

. Legyen mivel

. A bizonyítás első részében leírt lépéseket folytatva: , .


SPECIFIKÁCIÓ

6

Leggyengébb előfeltétel Legyen

állítás. Ekkor az S program

program,

leggyengébb előfeltétele az az

utófeltételhez tartozó

függvény, amelyre: és

.

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: . függvény, a kompozíció és a szigorú kompozíció megegyezik, tehát következő az állítás:

Mivel 1.

. tulajdonságai

Az

Legyen

állítások. Ekkor

program,

1.

(csoda kizárása elv)

,

2. ha

, akkor

(monotonitás tulajdonság)

,

3.

,

4.

.

Specifikáció tétele Legyen

feladat, B az F egy paramétere,

,

, F=

. Legyen

, és definiáljuk a következő állításokat: , . Ekkor ha

, akkor az S program megoldja F feladatot.

*Bizonyítás 1.

, ugyanis: Legyen

tetszőleges. Ekkor

és

relációk definíciója miatt

De ekkor a tétel feltételek alapján: 2.

és

.

, ugyanis: Legyen

tetszőlegesen rögzített,

olyan, amelyre .


. Ekkor a feltétel szerint:

.

SPECIFIKÁCIÓ

7

Jó specifikáció Ha a feladat specifikációjának felírásakor úgy választjuk meg a paramétertere és az elő-, utófeltételt, hogy rájuk a következő két feltétel teljesüljön: 1.

,

2.

vagy

és

,

akkor a specifikáció tételek meg fordítható. *Bizonyítás Azt kell belátni, hogy ha S megoldása F-nek, akkor: a. b.

.

Az a. következik abból, hogy 1. teljesülése esetén , akkor

a b. pedig, abból, hogy ha

, és a megoldás miatt

ugyanis 2. miatt az unió egy tagú, vagy minden tagja egyenlő. Az állítás két feltételének megfelelő specifikáció jó specifikáció. Létezik minden feladat esetén ilyen? Ha a paramétertér az állapottér,

az identikus leképezés és

, akkor az állítás mindkét feltétele

nyilvánvalóan teljesül. Változó Az A=

állapottér

egydimenziós projekciós függvényeit változónak nevezzük.

Ha a paramétertér is direktszorzat alakú, akkor a paramétertér egydimenziós projekciós függvényeit paraméterváltozóknak nevezzük.


SZEKVENCIA

8

Szekvencia Legyen

,

.

Legyenek

relációt az

programok.

és

szekvenciájának nevezzük és

-vel jelöljük, ha és

.

Szekvencia programfüggvénye Legyen A tetszőleges állapottér,

programok A-n, S=

. Ekkor

.

*Bizonyítás Legyen

tetszőleges. Ekkor

tehát

.

Legyen

. Ekkor

. A szekvencia levezetési szabálya Legyen S=

, és adott

állítás A-n. Ha

és

1) 2)

, akkor

.

*Bizonyítás Legyen

és

. Ekkor 1) miatt

. Mivel 2) miatt

. Továbbá 2) miatt

, tehát

.

A szekvencia levezetési szabálya és a specifikáció tétele alapján a következőt mondhatjuk: ha olyan programok, amelyekre a paramétertér teljesül, akkor

megoldja a

pontjában

párokkal adott feladatot.


és

és

ELÁGAZÁS

9

Elágazás feltételek,

Legyenek -kből képzett,

az

relációt

programok -n. Ekkor az

-k által meghatározott elágazásnak nevezzük, és

-nel

jelöljük, ha

ahol és Az elágazás programfüggvénye Legyen A tetszőleges állapottér, feltételek A-n.

programok, valamint . Ekkor

  Az elágazás levezetési szabálya , és adott

Legyen 1) 2)

állítás A-n. Ha

, akkor

.

*Bizonyítás Legyen Ekkor

, és tegyük fel, hogy valamelyik feltétel igaz -ra, azaz

.

, ugyanis .

Másrészt mivel

azaz

:

.


ELEMI PROGRAMOK

10

Elemi program Eleminek nevezünk egy

állapottéren egy

programot, ha .

SKIP -nek nevezzük azt a programot, amelyre

.

ABORT -tal jelöljük azt a programot, amelyre

.

Értékadás és

Legyen

. Az

program általános értékadás, ha

Az általános értékadáson belül speciális eseteket különböztetünk meg: 

Ha



Ha az



Ha

, akkor



Ha

és

, akkor az

programot értékkiválasztásnak nevezzük. (

reláció függvény, akkor az

programot értékadásnak nevezzük. (

) )

parciális értékkiválasztás.

determinisztikus ( parciális függvény), akkor

parciális értékadás.

Elemi programok programfüggvényei: 1. 2. 3. 4.

Elemi programok legggyengébb előfeltétele Mivel a

program programfüggvénye identikus leképezés, egy tetszőleges

tartozó leggyengébb előfeltétele:

Mivel az A tetszőleges

utófeltételhez

.

program programfüggvénye üres – a leggyengébb előfeltétel alapján egy 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 parciális esetben.


ELEMI PROGRAMOK Ha

függvény, akkor

11 függvény, és ezért

.

Ha

parciális függvény, tehát az értékadás parciális, akkor ennek leggyengébb előfeltétele:

Ha

nemdeterminisztikus. Feltesszük, hogy

, az értékkiválasztás leggyengébb előfeltétele

Parciális esetben:


TÍPUS

12

Típusspecifikáció hármast típusspecifikációnak nevezzük, ha teljesülnek rá a következő tételek:

A 1.

az alaphalmaz s specifikációs invariáns

2.

a típusérték halmaz

3.

a típusműveletek specifikációja, ahol

4.

, úgyhogy

.

Típus hármast típusnak nevezzük, ha az alábbi feltételek teljesülnek rá:

A

a reprezentációs függvény (reláció),

1.

a típusérzék halmaz az elemi típusérték halmaz típusinvariáns

2. 3.

, ahol

úgy, hogy

program, és

Megoldás

-n keresztül program a -n keresztül megoldja az

Azt mondjuk, hogy az vannak olyan

és

illeszkedő terek, amelynek altere , illetve , hogy a fenti értelemben definiált leképezés,

-nek, ahol

az

Megfelelés Egy

típus megfelel a

típusspecifikációnak, ha

1. 2.

-n keresztül megoldja -et.


szerint megoldása

kiterjesztése -re,

kiterjesztése -re.

az

feladatot, ha

pedig

TÍPUS

13

Típusspecifikáció tétele és

Legyen

adott típusspecifikáció és típus, és tegyük fel, hogy a

reprezentáció helyes, azaz

. Legyen továbbá

, elő- és utófeltétele pedig

és

, az

állapottere , egy paramétere

. és tegyük fel, hogy

. Legyen

állapottere illesztkedik

állapotteréhez. Definiáljuk a következő állításokat: ,

,ahol

a program és a feladat állapottere közötti, a -n keresztüli

megoldás definíciójában szereplő leképezés. Ekkor ha program a -n keresztül megoldja az

, akkor az

feladatot.

*Bizonyítás: A reláció szerinti megoldás tétele miatt csak azt kell belátnunk, hogy nyilvánvaló, mivel föltettük, hogy

teljesül. Ez pedig

.

Megfelelés általánosítása típus – általános értelemben – megfelel a

Azt mondjuk, hogy

típusspecifikációnak, ha létezik olyan ekvivalens típusspecifikáció, amelynek az eredeti értelemben megfelel. Absztrakt típus Legyen

egy típus. A

-t

absztrakt típusának nevezzük, ha

1. 2.

.


ALAPFOGALMAK 1. A reláció az program programfüggvénye, ha. Azt mondjuk, hogy az feladat szigorúbb, mint az feladat, ha

Recommend Documents