Szlávi Péter

Programozási tételek egymásra építése
*
Programtranszformációk

2000

Tartalom

A Cél, alapvető definíciók. 3

Program- és kódtranszformáció. 3

Függvény és implementációja – a függvényeljárás kiszámítása. 3

Szimmetrikus és aszimmetrikus logikai műveletek. 5

Programtranszformációk. 6

PT1. Függvénykompozíció. 6

PT2. Értékadások cseréje. 6

PT3. Párhuzamos értékadás I. 6

PT4. Párhuzamos értékadás II. 7

PT5. Feltételcsere logikai kifejezésben. 7

PT6. Az ’és’ és az ’és még’ ekvivalenciája. 7

PT7. ’és’-feltételszétbontás az elágazásban I. 7

PT8. ’vagy’-feltételszétbontás az elágazásban II. 7

PT9. Feltétel kiemelése elágazásból 8

PT10. Ciklusok összevonása. 8

PT11. Függvény kiemelése a ciklusfeltétel „belsejéből”. 8

PT12. Ciklusfeltétel részbeni kiemelése – indextúllépés elkerülésére I. 9

PT13. Ciklusfeltétel részbeni kiemelése – indextúllépés elkerülésére II. 9

PT14. Utolsó elem vizsgálatának kiemelése a ciklusfeltételből 9

PT15. Elágazások transzformálása I. 10

PT16. Elágazások transzformálása II. 10

PT17. Azonos utasítások kiemelése elágazás mindkét ágából 10

Tételek egymásra építése. 11

Az összeépítésben szereplő tételek. 11

Az összeépítés lépései általános esetben. 13

1. Másolással összeépítés. 14

2. Megszámolással összeépítés. 22

3. Maximum-kiválasztással összeépítés. 25

A Cél, alapvető definíciók

Program- és kódtranszformáció

A tételek ismeretében már a feladatok zöme mechanikusan megoldható a specifikáció alapján^[1], a struktúraszerinti feldolgozás elve segítségével és a programozási tételek alkalmazásával. Az egészen triviális feladatokat kivéve, a megoldás több tétel ötvözete lesz. A mechanikus tételalkalmazás –természetesen– nem adhat általában optimális megoldást. Keletkezhetnek józanésszel is javítható „algoritmikus redundanciák” (bántó kódismétlések, nyilvánvalóan elkerülhető segédváltozók stb.), amelyeket részek összevonásával, átstrukturálással korrigálni lehet.

Annak érdekében, hogy ez az optimalizáló lépés megtartsa a tételek nyújtotta „garantált” helyességet, de elérje a kívánt hatékonysági célt is, kidolgozunk néhány –az esetek többségében alkalmazható– átalakítási szabályt, ún. programtranszformációt.

A programok transzformálásának lehet egy másik célja is. Amikor egy adott programozási nyelvre kódolásnál tartunk, sokszor az algoritmus „nagystílűsége” miatt kényszerülünk bizonyos transzformációra. Itt tehát egy programozási nyelv „szószátyársága” erőszakolja ki a változtatást, nem az algoritmusban eleve meglévő lehetőségek. A programnak e két céllal történő átalakítását megkülönböztetjük egymástól, az utóbbira a kódtranszformáció kifejezést fogjuk alkalmazni. Most csak az előbbi célú átalakítással foglalkozunk.

Függvény és implementációja – a függvényeljárás kiszámítása

A könnyebb megfogalmazás miatt bevezetünk néhány fogalmat, ill. egy-két értelmező megjegyzést bocsátunk előre.

Az alábbiakban a függvény alatt mindig valamely f (kisbetűkkel jelölt) „absztrakt” függvényt kiszámító F (nagybetűkkel jelölt) függvényeljárást értünk, amely kiszámítási sémájára vonatkozólag feltételezéseket teszünk. Maguk az „absztrakt” függvények egyértékűek, és a hozzájuk tartozó függvényeljárások explicite tartalmazzák azokat a paramétereket, amelyektől függnek, vagyis nincsenek „latens” paraméterei (pl. valamely globálisan deklarált adat).

Elvárásunk látszólag magától értetődő: y¬f(x) „absztrakt” utasításnak minden körülmények között megfeleljen az algoritmusbeli y:=F(x).

f: X®Y

Þ

Függvény F(^[2]x:TX):TY Változó y:TY … y:=f(x) … [f(x) kiértékelése, amely közben x is módosulhat] F:=y Függvény vége.

A lényeg: először az f(x) kiértékelése történik meg, majd a legvégén az értékvisszaadás. Így ha volna mellékhatás^[3], a függvény értéke a ténylegesen kiszámított érték lesz minden zavaró körülmény ellenére. Azaz nem interferál a függvényérték és a paraméter.

Ezzel az értelmezéssel kikerülhető az a bizonytalanság, ami egyébként lenne az alábbi utasításnál (ha a mellékhatás megengedett): x:=F(x) Milyen értékkel rendelkezik az értékadás után az x?

Például:

x:=2 x:=F(x) {x=?}

Függvény F(Változó x:Egész):Egész Változó y:Egész y:=2*x; x:+1 F:=y Függvény vége.

Definíció: (x-invariancia)

Egy f: X´Y®Z, f(x,y) leképezést megvalósító F(x,y) függvényeljárást x-invariánsnak (első változó szerint invariánsnak) nevezünk, ha "(x,y)ÎDom_f: x'=x.

Ahol Dom_f az f függvény értelmezési tartományát jelöli, az x' pedig az x (F(x,.)) kiszámítás utáni értékét.

Világos, hogy egy x-invariáns f függvény F-beli x paraméterének nyugodtan adható konstans hozzáférési jog, hiszen bemeneti a funkciója.

E fogalom birtokában már megfogalmazhatjuk a két- vagy többváltozós függvények kiszámítására vonatkozó elvárásainkat:

f: X´Y®Z, $g,h,i:X´Y®Z : g,h,i x- és y-invariánsok Ù f(x,y)=i(x,y) Ù x’=g(x,y) Ù y’=h(x,y)

Þ

Függvény F(Változó x:TX, y:TY):TZ Változó xx:TX, yy:TY, z:TZ xx:=G(x,y); yy:=H(x,y) z:=I(x,y) x:=xx; y:=yy F:=z Függvény vége.

A lényeg: először az esetlegesen módosuló paraméterek értékeit számítjuk ki, majd az eredeti bemenő értékekkel a „lényegi” számítást, a függvény értékét. (Innen már sejthető, hogy több paraméteres függvények kiszámításával szemben milyen elvárásaink lehetnek.)

Definíció: (x-függetlenség)

Egy f: X´Y®Z, f(x,y) leképezést megvalósító F(x,y) függvényeljárást x-függetlennek (első változójától függetlennek) nevezünk, ha x-invariáns és "x,xxÎX, "yÎY: (x,y),(xx,y)ÎDom_f: f(x,y)=f(xx,y).

Nyilvánvaló, hogy ha egy F(x,y) x-független, akkor alkalmazható az F(y) jelölés. Ezért indokolni kell e fogalom bevezetésének értelmét! Íme: időnként szükség lesz bizonyos segédváltozók bevezetésére, de ezt a többi programrésszel való zavartalan együttműködés garantálásával (interferenciamentesség megtartásával) szabad csak végrehajtani. Ebben a szituációban a megfelelő segédváltozó néven nevezéséhez kell fölhasználni.

Szimmetrikus és aszimmetrikus logikai műveletek

A későbbiek során fontos lesz az, hogy egy ’és’, ill. egy ’vagy’ logikai művelet szimmetrikus, vagy „értelmesen” aszimmetrikus működésű-e, ezért ezeket a leírásban meg fogjuk különböztetni. Gondoljunk csak például az ’Eldöntés tétel’-beli ciklusfeltételére, amit „egészében” ’i=N+1’ esetén aggályos lenne végrehajtani, hacsak nem ’aszimmetrikus és’-t feltételezünk. Mindazon által az is világos, hogy egy olyan logikai feltételben, amelynek –mondjuk– második tényezője egy mellékhatással rendelkező^[4] függvényt tartalmaz, akkor ennek végrehajtására mindenképpen szükség van. Ezzel indokoljuk, hogy mindkettőre szükség van, de célszerű világos megkülönböztetésükre is.

Továbbiakban a logikai műveleti jeleket az alábbi értelmezéssel fogjuk használni:

Logikai művelet	Az aszimmetrikus jelölése	A szimmetrikus jelölése
Ù	és[SzP1]	és még
Ú	vagy	vagy különben

Programtranszformációk

Programtranszformáció alatt (a programozási tételhez hasonlóan) egy állítást értünk, amely két program(darab) azonosságát[SzP2] állítja egy feltétel teljesüléséhez kötve.

Az alábbiakban fölsoroljuk a legfontosabb programtranszformációkat (PTx), amelyekhez közöljük –természetesen–, hogy milyen feltételek (efPT) mellett alkalmazhatók. (A feltételek nem feltétlenül lesznek a „legbővebb bemenetet” megengedők.)

PT1. Függvénykompozíció

efPT: G(y) y-invariáns Ù P(x,z,y) y-független

y:=F(x); z:=G(y) w:=P(x,z,y)

Û

z:=G(F(x)) w:=P(x,z,y)

Megjegyzés:

Vegyük észre, hogy 1) az első feltétel (G(y) y-invariáns) „pusztán” formális okok miatt kell, nevezetesen ahhoz, hogy a jobboldali transzformációban az F függvény a G-be behelyettesíthető legyen. 2) a második (P(x,z,y) y-független) pedig a („folytatólagos”) környezettel való interferenciamentességet jelenti; egyszerűen szólva: az y zavarmentes beilleszthetőségét (fordított irányban: elhagyhatóságát).

PT2. Értékadások cseréje

efPT: F(x), G(x) x-invariáns

y:=F(x); z:=G(x)

Û

z:=G(x); y:=F(x)

Megjegyzés:

Vegyük észre, hogy e szerint az ’A(x,y); B(x,z)’ eljárások cseréjét is elvégezhetjük, ha ők x-invariánsok. Ui. ez épp azt jelenti, hogy paraméterei szétválaszthatók csak bemenetire, ill. „másra”.

PT3. Párhuzamos értékadás I.

efPT: F(x,y) y-invariáns Ù G(x,y) x-invariáns Ù P(x,y,sx,sy) sx-, sy-független

x,y:=F(x,y),G(x,y) w:=P(x,y,sx,sy)

Û

sx:=x; sy:=y x:=F(x,y); y:=G(sx,sy) w:=P(x,y,sx,sy)

Megjegyzés:

A végrehajtás párhuzamossága (a baloldali programdarabban) azt jelenti, hogy az utasítás után teljesül az alábbi állítás:

x’=F(x,y) Ù y’=G(x,y)

Figyelem: az F(x,y) y-invaranciája [SzP3] és a G(x,y) x-invarianciája a párhuzamos végrehajtásnak, s nem a programtranszformáció alkalmazhatóságának a feltétele!

PT4. Párhuzamos értékadás II.

efPT: F(x,y) y-invariáns [Ù G(x,y) x-invariáns^[5]] Ù P(x,y,sx) sx-független

x,y:=F(x,y),G(x,y) w:=P(x,y,sx)

Û

sx:=x x:=F(x,y); y:=G(sx,y) w:=P(x,y,sx)

PT5. Feltételcsere logikai kifejezésben

efPT: F(x), G(x) x-invariáns

l:=F(x) és G(x)

Û

l:=G(x) és F(x)

Megjegyzés:

Hasonló programtranszformáció fogalmazható meg az ’és még’ tényezőinek fölcserélhetőségére is.

PT6. Az ’és’ és az ’és még’ ekvivalenciája

efPT: G(x) x-invariáns

l:=F(x) és G(x)

Û

l:=F(x) és még G(x)

Megjegyzés:

Hasonló programtranszformáció tartozik a ’vagy’ és a ’vagy különben’ azonosságához is.

Fontos következmény: ha tehát a tényezők mellékhatás-nélküli[SzP4] kifejezések, akkor nincs jelentősége annak, hogy szimmetrikus (’és még’/’vagy különben’) vagy aszimmetrikus (’és’ /’vagy’) kapcsolja őket össze! Sőt azt is látni kell, hogy a logikai kifejezés bárhol (pl. elágazás, vagy ciklus feltételében) szerepelhet. (Lényegében csak a „nyomaték kedvéért” fogalmazzuk meg ezt a PT7-ben, PT8-ban.)

PT7. ’és’-feltételszétbontás az elágazásban I.

efPT: G(x) x-invariáns

Ha F(x) és G(x) akkor z:=H(x) különben z:=I(x)

Û

Ha F(x) és még G(x) akkor z:=H(x) különben z:=I(x)

Megjegyzés:

A cím arra utal, hogy (a baloldali algoritmusban) az ’és’ művelet megvalósítható a feltételek szétbontásával így is:

Ha F(x) akkor
Ha G(x) akkor ...IGAZ-ÁG (igaz–F(X)–G(X))...
különben ...HAMIS-ÁG (igaz–F(X),hamis–G(X))...
különben ...HAMIS-ÁG (hamis–F(X))...

PT8. ’vagy’-feltételszétbontás az elágazásban II.

efPT: G(x) x-invariáns

Ha F(x) vagy G(x) akkor z:=H(x) különben z:=I(x)

Û

Ha F(x) vagy különben G(x) akkor z:=H(x) különben z:=I(x)

Megjegyzés:

A cím itt is arra utal, hogy (a baloldali algoritmusban) a ’vagy’ művelet megvalósítható a feltételek szétbontásával így is:

Ha nem F(x) akkor
Ha G(x) akkor ...IGAZ-ÁG (hamis–F(X),igaz–G(X))...
különben ...HAMIS-ÁG (hamis–F(X),hamis–G(X))...
különben ... IGAZ-ÁG(igaz–F(X))...

PT9. Feltétel kiemelése elágazásból

efPT: F(x) x-invariáns Ù G(x,s) s-független Ù T(x) x-invariáns

Ha T(F(x)) akkor y:=F(x) z:=G(x,s)

Û

s:=F(x) Ha T(s) akkor y:=s z:=G(x,s)

Megjegyzés:

A G függvény „egyesíti” magában a program elágazás utáni részének össztranszformációját. A feltételből kiolvasható, hogy az ’s’ változót semmire sem használja, így bátran választható segédváltozóként. A G(x,s) s-függetlensége a baloldali algoritmus alkalmazhatóságának a feltétele.

PT10. Ciklusok összevonása

efPT: L(x), M(x), G(x,y), H(x,z), Cf(x) x-invariáns

x:=k; y:=L(x) Ciklus amíg Cf(x) y:=G(x,y); x:=I(x) Ciklus vége x:=k; z:=M(x) Ciklus amíg Cf(x) z:=H(x,z); x:=I(x) Ciklus vége

Û

x:=k; y:=L(x); z:=M(x) Ciklus amíg Cf(x) y:=G(x,y); z:=H(x,z); x:=I(x) Ciklus vége

Megjegyzés:

Mint látható: az x tölti be a ciklusváltozó szerepét, az L és M függvények a kezdőértékek beállítását végzik, az I –közös– függvény pedig a ciklusok szervezését, a G és H függvények „lényegi” (az y-ra, ill. a z-re vonatkozó) transzformációkat.

PT11. Függvény kiemelése a ciklusfeltétel „belsejéből”

efPT: G(x,y,fx) fx-független Ù T(x) x-invariáns

Ciklus amíg T(F(x)) y:=Cm(x,y) Ciklus vége z:=G(x,y,fx)

Û

fx:=F(x) Ciklus amíg T(fx) y:=Cm(x,y); fx:=F(x) Ciklus vége z:=G(x,y,fx)

Megjegyzés:

A G függvény a program „utóéletét” szimbolizálja, amely során az fx változót nem, viszont akár x, akár y értékét fölhasználhatja. A T(x) x-invarianciája a baloldali transzformáció formális feltétele.

Vegyük észre, hogy a ciklus vezérlését (azaz az x módosítását) két függvény együttese végzi: az F(x) és a Cm(x,y).

PT12. Ciklusfeltétel részbeni kiemelése – indextúllépés elkerülésére I.

efPT: e£v Ù $Előző(e) Ù [$Következő(v)] Ù T(x) [, Következő(x)] x-invariáns

x:=e Ciklus amíg x£v és nem T(x) x:=Következő(x) Ciklus vége l:=x£v

Û

x:=Előző(e); l:=Hamis Ciklus amíg x<v és nem l x:=Következő(x); l:=T(x) Ciklus vége

Megjegyzés:

A programdarabokban szereplő x (ciklust vezérlő) változó típusa rendezett, amelyen értelmezve van az Előző és a Következő függvény (nevükből kihámozható szemantikával)^[6].

A Következő(v) létezése nem a programtranszformáció feltétele, hanem a baloldali algoritmus működésének.

Ha e£v feltételt elhagyjuk az efPT-ből, akkor (e>v esetben) a két algoritmus l szempontjából ekvivalens ugyan, de x szempontjából nem.

PT13. Ciklusfeltétel részbeni kiemelése – indextúllépés elkerülésére II.

efPT: e£v Ù T(x) [, Következő(x)] x-invariáns [Ù $Következő(v)]

x:=e Ciklus amíg x£v és nem T(x) x:=Következő(x) Ciklus vége l:=x£v

Û

x:=e; l:=T(x) Ciklus amíg x<v és nem l x:=Következő(x); l:=T(x) Ciklus vége

Megjegyzés:

A Következő(v) létezése nem a programtranszformáció feltétele, hanem a baloldali algoritmus működésének.

PT14. Utolsó elem vizsgálatának kiemelése a ciklusfeltételből

efPT: T(x) [, Következő(x)] x-invariáns [Ù $Következő(v)]

x:=e Ciklus amíg x£v és még nem T(x) x:=Következő(x) Ciklus vége l:=x£v

Û

x:=e Ciklus amíg x<v és még nem T(x) x:=Következő(x) Ciklus vége l:=T(x)

Megjegyzés:

Az előző megjegyzés itt is érvényes.

PT15. Elágazások transzformálása I.

efPT: "iÎ[1..N]: F_i(x), P_i(x,y) x-invariáns Ù "x: "i¹j: Ø(F_i(x)ÙF_j(x))

Ha F1(x) akkor P1(x,y) Ha F2(x) akkor P2(x,y) … Ha FN(x) akkor PN(x,y)

Û

Elágazás F1(x) esetén P1(x,y) F2(x) esetén P2(x,y) … FN(x) esetén PN(x,y) Elágazás vége

Megjegyzés:

Az előfeltétel utolsó részében azt fogalmaztuk meg, hogy a feltételek páronként egymást kizáróak, azaz bármely x-re legfeljebb egy feltétel teljesülhet.

PT16. Elágazások transzformálása II.

efPT: F(x), P(x,y), Q(x,y) x-invariáns

Ha F(x) akkor P(x,y) különben Q(x,y) Ha F(x) akkor R(x,y) különben S(x,y)

Û

Ha F(x) akkor P(x,y); R(x,y) különben Q(x,y); S(x,y)

Megjegyzés:

Az előfeltétel utolsó részében azt fogalmaztuk meg, hogy a feltételek páronként egymást kizáróak, azaz bármely x-re legfeljebb egy feltétel teljesülhet.

PT17. Azonos utasítások kiemelése elágazás mindkét ágából

efPT: F(x) x-invariáns

Ha F(x) akkor P(x,y); Q(x,y); R(x,y) különben P(x,y); S(x,y); R(x,y)

Û

P(x,y) Ha F(x) akkor Q(x,y) különben S(x,y) R(x,y)

Megjegyzés:

Az előfeltételbeli x-invariancia kizárólag a P előre emeléséhez kell.

Tételek egymásra építése

Az összeépítésben szereplő tételek

Az alábbiakban csak azokat a tételeket adjuk meg, amelyek fontos szerepet kapnak a fő témánk, a tételek összeépítése szempontjából. Mindegyik kap egy azonosítót, amellyel a későbbiek során rövidíthetjük a rájuk történő hivatkozást. (Pl. MT=Másolás Tétel...)

Legelőször is a tételt, mint leképezést írjuk le az értelmezési tartományával és az értékkészletével.^[7] Azután e megadást pontosítjuk (specifikáljuk) a bemenet, a kimenet, az elő- és utófeltételével. A specifikációt kielégítő (egy lehetséges) megoldás algoritmusával zárjuk a tételt. Az algoritmust, mint eljárást definiáljuk, amelynek föltüntetjük a bemeneti és a kimeneti adatait. (De itt más az esetleges „kívülről örökölt”, feladat megfogalmazta függvényparamétereket nem.) A tétel helyességének bizonyításától ebben a részben eltekintünk.

MT: Másolás(N,H^*,H®G):G^*

Be: NÎN, XÎH^*, f:H®G

Ki: YÎG^*

Ef: N=Hossz(X)

Uf: "i(1£i£N): y_i=f(x_i) [ÞHossz(Y)=N]

Az algoritmus:

Eljárás Másolás(Be:^[8] N:PozEgész,X:Tömb(1..N:H_elemTíp)^[9],
Ki: Y:Tömb(1..N:G_elemTíp)):

Ciklus I=1-től N-ig
Y(I):=f(X(I))
Ciklus vége
Eljárás vége.

ST: Sorozatszámítás(N,H^*,G,GxH®G):G

Be: NÎN, XÎH^*, F:H^*®G

Ki: SÎG

Ef: N=Hossz(X) Ù $F₀ÎG Ù $f:GxH®G Ù

F(x₁,...,x_N)=f(F(x₁,...,x_N-1),x_N) Ù F()=F₀

Uf: S=F(x₁,...,x_N)

Az algoritmus:

Eljárás Sorozatszámítás(Be: N:PozEgész,X:Tömb(1..N:H_elemTíp),
Ki: S:G_elemTíp):

S:=F₀
Ciklus I=1-től N-ig
S:=f(S,X(I))
Ciklus vége
Eljárás vége.

KT: Keresés(N,H^*,H®L):(L,N)

Be: NÎN, XÎH^*, T:H®L

Ki: VANÎL, SORSZÎN

Ef: N=Hossz(X)

Uf: VAN º ($i (1£i£N): T(x_i)) Ù
VAN Þ 1£SORSZ£N Ù T(x_SORSZ)

Az algoritmus:

Eljárás Keresés(Be: N:PozEgész,X:Tömb(1..N:H_elemTip),
Ki: VAN:Logikai,SORSZ:PozEgész):

I:=1
Ciklus amíg I£N és nem T(X(I))
I:+1
Ciklus vége
VAN:=(I£N)
Ha VAN akkor SORSZ:=I
Eljárás vége.

MszT: Megszámolás(N,H^*,H®L):N

Be: NÎN, XÎH^*, T:H®L

Ki: DBÎN

Ef: N=Hossz(X)

Uf:

Def^[10]: c:L ®{0,1},

Az algoritmus:

Eljárás Megszámolás(Be: N:PozEgész,X: Tömb(1..N:H_elemTip),
Ki: DB:PozEgész):

DB:=0
Ciklus I=1-től N-ig
Ha T(X(I)) akkor DB:+1
Ciklus vége
Eljárás vége.

MxT: Maximumkiválasztás(N,H^*,HxH®L):N

Be: NÎN, XÎH^*, H rendezett halmaz (Þ$<,£ relációk)

Ki: MAXÎN

Ef: N=Hossz(X) Ù N³1

Uf: 1£MAX£N Ù "i(1£i£N): x_MAX³x_i

Az algoritmus:

Eljárás Maximumkiválasztás(Be: N:PozEgész,X:Tömb(1..N:H_elemTip),
Ki: MAX:PozEgész):

MAX:=1
Ciklus I=2-től N-ig
Ha X(MAX)<X(I) akkor MAX:=I
Ciklus vége
Eljárás vége.

KvT: Kiválogatás(N,H^*,H®L):(N,N ^*)

Be: NÎN, XÎH^*, T:H®L

Ki: DBÎN, YÎN^*

_Ef: N=Hossz(X)

Uf: Ù YÎ[1..N]^DB Ù Halmazfölsorolás(Y)
Ù "iÎ[1..DB]: T(x_yi)

Az algoritmus:

Eljárás Kiválogatás(Be: N:PozEgész,X:Tömb(1..N:H_elemTip),
Ki: M:PozEgész,Y:Tömb(1..M:NemNegEgész)):

M:=0
Ciklus I=1-től N-ig
Ha T(X(I)) akkor M:+1; Y(M):=I
Ciklus vége
Eljárás vége.

Az összeépítés lépései általános esetben

1. A feladat specifikációjának elkészítése (bemenet, kimenet, elő- és utófeltétel).

2. Az utófeltétel felbontása programozási tételek utófeltételeire (esetleg segédváltozók, -függvények bevezetésével).

3. A felbontás helyességének bizonyítása.

4. A tételek „mechanikus” alkalmazása a részspecifikációk alapján.

5. Az algoritmus rövidítése (segédváltozók kiküszöbölése, segédfüggvény törzsének direkt beillesztése) programtranszformációk alkalmazásával.

A következőkben néhány gyakori esetet tárgyalunk példa gyanánt. Ezen minták alapján bárki elkészíthet jó néhány további tételkombinációt. Kiindulópontként érdemes a tételspecifikációk fejsoraként alkalmazott szignatúrákat figyelembe venni: hogy a formális szempontból egyáltalán elképzelhető kombinációkat földerítsük.

1. Másolással összeépítés

Másolással bármelyik programozási tétel egybeépíthető, hiszen csupán annyi a teendő, hogy a programozási tételben szereplő x_i bemenő adatra hivatkozást kicseréljük valamilyen g-transzformált x_i-re (g(x_i)).

Ha például egy számsorozat elemeinek négyzetösszegét kellene megadnunk, az egy másolást (számokhoz számok négyzeteinek vagy –általánosan: valamely:– g-transzformáltjainak a rendelése) és egy sorozatszámítást (pl. összegzést) tartalmaz. Nézzük meg e két tétel általános egymásra építését!

1. lépés: a specifikáció elkészítése:

Be: NÎN, XÎH^*, F:G^*®E, g:H®G

Ki: SÎE

Ef: N=Hossz(X) Ù $F₀ÎE Ù $f:E´G®E Ù
F(y₁,...,y_N)=f(F(y₁,...,y_N-1),y_N) Ù
F()=F₀

Uf: S=F(g(x₁),...,g(x_N))

2. lépés: az utófeltétel felbontása:

Uf Û S=F(y₁,...,y_N) (1)
Ù
"i(1£i£N): y_i=g(x_z) (2)

3. lépés: a felbontás helyességének belátása:

Triviálisan igaz: az (1)-be történő ’y_i¬g(x_i)’ behelyettesítéssel az Uf-t kapjuk.

(A behelyettesítés után:
S=F(g(x₁),..., g(x_N)) (1)
Ù
"i(1£i£N): g(x_i)=g(x_i) (2)
(2) azonosság, így elhagyható, (1) meg maga az Uf.)

4. lépés: a „naiv” algoritmus generálása:

Az (1) az Y sorozatra vonatkozó ST utófeltétele. A (2) pedig az MT X-re vonatkozó utófeltétele. Mivel ez utóbbi operál a bemeneti sorozattal, ezért először azt kell alkalmazni. Ennek eredménye lesz az ST bemeneti Y sorozata. Tehát a két tétel egymásután alkalmazása

S:=Sorozatszámítás(N,Másolás(N,X,g),F₀,f)

szolgáltatja az alábbi megoldást:

Eljárás SorozatosMásolás(Be: N:PozEgész,X:Tömb(1..N:H_elemTíp),
Ki: S:E_elemTíp):

...
Ciklus I=1-től N-ig
Y(I):=G(X(I))
Ciklus vége
S:=F₀
Ciklus I=1-től N-ig
S:=f(S,Y(I))
Ciklus vége
Eljárás vége.

5. lépés: az algoritmus „naivitásának” megszüntetése:

Az ’amíg-os’ ciklusra átírás után PT10 miatt –mivel jelen esetben teljesülnek a feltételei– átalakítható az alábbi hatékonyabb és egyszerűbb alakúvá, persze a ’számlálásos’ ciklusra visszatérés után:

...
S:=F₀
Ciklus I=1-től N-ig
Y(I):=G(X(I))
S:=f(S,Y(I))
Ciklus vége
...

A PT1 miatt tovább egyszerűsíthető (értékadások egyesítése, Y kiküszöbölése):

...
S:=F₀
Ciklus I=1-től N-ig
S:=f(S,G(X(I)))
Ciklus vége
...

Második példaként vegyük a másolás és a maximum-kiválasztás összeépítését! Ebben a maximális elem értékét és indexét is meghatározzuk. (Az előző feladat analógiájára ilyen lehet a legnagyobb abszolútértékű szám abszolútértékének meghatározása egy számsorozatból. Általánosság kedvéért az abszolútérték függvény helyett legyen egy g, amelyet a G implementál az algoritmusban.)

1. lépés: a specifikáció elkészítése:

Be: NÎN, XÎH^*, C rendezett halmaz (Û$<,£ relációk),

g:H®C

Ki: MAXÎN, MAXÉRTÎH

Ef: N=Hossz(X) Ù N³1

Uf: MAXÎ[1..N] Ù "iÎ[1..N]: g(x_MAX)³g(x_i) Ù

MAXÉRT=g(x_MAX)

2. lépés: az utófeltétel felbontása:

Uf Û MAXÎ[1..N] Ù "iÎ[1..N]: y_MAX³y_i (1)
Ù
"iÎ[1..N]: y_i=g(x_i) (2)
Ù
MAXÉRT=y_MAX (3)

3. lépés: a felbontás helyességének belátása:

Triviálisan igaz: az (1), (3)-ba történő ’y_i¬g(x_i)’ behelyettesítéssel az Uf-t kapjuk.

4. lépés: a „naív” algoritmus generálása:

Az (1) az MxT Y sorozatra vonatkozó utófeltétele. A (2) pedig az MT X-re vonatkozó utófeltétele, (3) pedig –az értékadás szemantikája alapján– egy egyszerű értékadással megvalósítható. Mivel ismét a második tétel algoritmusa operál a bemeneti sorozattal, ezért először azt kell alkalmazni. Ennek eredménye lesz az MxT bemeneti Y sorozata. Tehát a két tétel egymásután alkalmazása

MAX:=Maximumkiválasztás(N,Másolás(N,X,g),<)

szolgáltatja megoldást. A MAXÉRT meghatározása már egy egyszerű értékadással megoldható.

Az algoritmikus megoldás „első olvasatban” tehát az alábbi lesz:

Eljárás MaximumosMásolás(Be: N:PozEgész,X:Tömb(1..N:H_elemTíp):
Ki: MAX:PozEgész, MAXÉRT: H_elemTíp):

...
Ciklus I=1-től N-ig
Y(I):=G(X(I))
Ciklus vége
MAX:=1
Ciklus I=2-től N-ig
Ha Y(MAX)<Y(I) akkor MAX:=I
Ciklus vége
MAXÉRT:=Y(MAX)
Eljárás vége.

5. lépés: az algoritmus „naivitásának” megszüntetése:

A PT10 miatt átalakítható az alábbi hatékonyabb és egyszerűbb alakúvá, feltéve, hogy az I=1 esetet különválasztjuk az első ciklustól:

...
Y(1):=G(X(1)); MAX:=1
Ciklus I=2-től N-ig
Y(I):=G(X(I))
Ha Y(MAX)<Y(I) akkor MAX:=I
Ciklus vége
...

Alakítsuk át a megoldást úgy, hogy az utófeltételben szereplő MAXÉRT=y_MAX formula invariáns állítás (azaz a ciklus akárhányadik lefutásakor igaz) legyen a teljes programban:

...
Y(1):=G(X(1)); MAX:=1; MAXÉRT:=Y(MAX)
Ciklus I=2-től N-ig
Y(I):=G(X(I))
Ha Y(MAX)<Y(I) akkor MAX:=I; MAXÉRT:=Y(MAX)
Ciklus vége
...

A PT1 2-szeres alkalmazásával a ciklus előtti utasítások drasztikusan egyszerűsíthetők:

Y(1):=G(X(1)); MAX:=1; MAXÉRT:=Y(MAX)
Þ
MAXÉRT:=G(X(1))),

A PT1 és a PT9 „visszafelé” alkalmazásával a ciklusmag egyszerűsíthető

Y(I):=G(X(I))
Ha Y(MAX)<Y(I) akkor MAX:=I; MAXÉRT:=Y(MAX)
Þ
Ha Y(MAX)<G(X(I)) akkor MAX:=I; MAXÉRT:=G(X(I))

Természetesen ezek után az Y(1)-re és a ciklusban az Y(I)-re vonatkozó értékadások már nincsenek:

...
MAX:=1; MAXÉRT:=G(X(1))
Ciklus I=2-től N-ig
Ha MAXÉRT<G(X(I)) akkor MAX:=I; MAXÉRT:=G(X(I))
Ciklus vége
...

Nézzünk meg egy újabb példát, amely akár alaptételként is előfordulhatna. A feladat. határozzuk meg egy X szám sorozat T-tulajdonságúak átlagát!

1. lépés: a specifikáció elkészítése:

Be: NÎN, XÎR^*, T:R®L

Ki: átlÎR

Ef: N=Hossz(X)

Uf: dbT= Ù
dbT¹0 Þ össz= Ù átl=össz/dbT Ù

dbT=0 Þ átl=0

Mint látható számos segédváltozót be vezettünk az Uf-ben: dbT, össz.

Ami már eddig is világos, hogy az algoritmus a dbT meghatározása után egy elágazást tartalmaz. Ennek különben ága (dbT=0 esetén) borzasztóan egyszerű: átl:=0. Vagyis a megoldás nagybani szerkezet így alakul:

dbT:=???
Ha dbT¹0 akkor össz:=???; átl:=össz/dbT (*)
különben átl:=0

A ??? részek azok, amik megfontolást igényelnek.

2. lépés: az utófeltétel felbontása:

Kétféleképpen is elkészítjük az Uf felbontását. Mindkettőben a tételeknél felismerhetetlen, furcsa, feltételes szumma megszüntetése a cél. Az elsőben, a már „klasszikus”, a segéd sorozat bevezetése módszert alkalmazzuk.

Uf’: dbT= Ù (1’)
"iÎ[1..N]: ((T(x_i) Þ y_i=x_i ) Ù (ØT(x_i) Þ y_i=0)) (2’)
dbT¹0 Þ
össz= Ù (3’)
átl=össz/dbT Ù (4’)

dbT=0 Þ
átl=0 (5’)

A másik átiratban egy segédfüggvényt (a c-függvényt) vezetünk be, illetve építünk be a szumma tagjaiba.

Uf”: dbT= Ù (1”)
dbT¹0 Þ
össz= Ù (2”)
átl=össz/dbT Ù (3”)

dbT=0 Þ
átl=0 (4”)

3. lépés: a felbontás helyességének belátása:

Ezt most elhagyjuk…

4. lépés: a „naiv” algoritmus generálása –Uf’-höz–:

Nézzük meg az elsőt! Ebben felismerhető a megszámolás tétel (1’), a másolás tétel (2’), a sorozatszámítás tétel (3’). A (4’) és az (5’) egy-egy értékadással algoritmizálható. A megoldás legfelsőbb szintje ugyanaz, amit korábban előrejeleztünk. A másolás tételbeli függvény itt könnyen belátható módon egy kétirányú elágazással valósítható meg. Vagyis:

Ha T(X(I)) akkor Y(I):=X(I) különben Y(I):=0

Figyelembe véve a korábbi algoritmusvázlatot (*), és a fentieket, kapjuk:

[MszT – megszámolás tétel alkalmazása:]
dbT:=0
Ciklus I=1-től N-ig
Ha T(X(I)) akkor dbT:+1
Ciklus vége
[MT – másolás tétel alkalmazása:]
Ciklus I=1-től N-ig
Ha T(X(I)) akkor Y(I):=X(I) különben Y(I):=0
Ciklus vége
Ha dbT¹0 akkor
[ST – sorozatszámítás tétel alkalmazása:]
össz:=0
Ciklus I=1-től N-ig
össz:=össz+Y(I)
Ciklus vége
átl:=össz/dbT
különben
átl:=0
Elágazás vége

5. lépés: az algoritmus „naivitásának” megszüntetése –Uf’-höz–:

Az első két tétel összevonása a PT10 segítségével elvégezhető.

[MszT – megszámolás és MT – másolás tétel alkalmazása:]
dbT:=0
Ciklus I=1-től N-ig
Ha T(X(I)) akkor dbT:+1
Ha T(X(I)) akkor Y(I):=X(I) különben Y(I):=0
Ciklus vége

Majd a PT16-tal egyesíthető a két, azonos feltételű elágazás:

[MszT – megszámolás és MT – másolás tétel alkalmazása:]
dbT:=0
Ciklus I=1-től N-ig
Ha T(X(I)) akkor dbT:+1; Y(I):=X(I)
különben Y(I):=0
Ciklus vége

Ahhoz, hogy bármi további transzformációra esélyünk legyen, ki kell emelni a sorozatszámítás tételt az elágazásból. Ez megtehető a PT17 szerint. A teljes algoritmus így adódik:

dbT:=0
Ciklus I=1-től N-ig
Ha T(X(I)) akkor dbT:+1; Y(I):=X(I)
különben Y(I):=0
Ciklus vége

[ST – sorozatszámítás tétel alkalmazása:]
össz:=0
Ciklus I=1-től N-ig
össz:=össz+Y(I)
Ciklus vége
Ha dbT¹0 akkor
átl:=össz/dbT
különben
átl:=0
Elágazás vége

Megint két azonos szervezésű ciklus következik egymásután. Most is összevonhatók a PT10 szerint.

dbT:=0; össz:=0
Ciklus I=1-től N-ig
Ha T(X(I)) akkor dbT:+1; Y(I):=X(I)
különben Y(I):=0
össz:=össz+Y(I)
Ciklus vége
Ha dbT¹0 akkor
átl:=össz/dbT
különben
átl:=0
Elágazás vége

Az első ciklusban a PT17 „fordított” alkalmazásával a ciklusmag második utasítását bevisszük az elágazás mindkét ágába:

Ha T(X(I)) akkor dbT:+1; Y(I):=X(I); össz:=össz+Y(I)
különben Y(I):=0; össz:=össz+Y(I)

A PT1 már szokásos bevetésével mind az akkor-, mind a különben-ágon két-két értékadást eggyé alakítunk:

Ha T(X(I)) akkor dbT:+1; össz:=össz+X(I)
különben össz:=össz+0

A különben elhagyható, hiszen valójában nem csinál semmit. Így kapjuk az alábbi teljes és végleges algoritmust:

dbT:=0; össz:=0
Ciklus I=1-től N-ig
Ha T(X(I)) akkor dbT:+1; össz:=össz+X(I)
Ciklus vége
Ha dbT¹0 akkor
átl:=össz/dbT
különben
átl:=0
Elágazás vége

A másik, Uf” specifikációban két tételt ismerhetünk föl: a megszámolás tételt (1”) és a sorozatszámítás tételt (2”). A (3”) és (4”) itt is egy-egy értékadással elérhető. Röviden gondoljuk végig az ebből kiinduló levezetést!

4. lépés: a „naiv” algoritmus generálása –Uf”-höz–:

A korábbiakat nem megismételve a „naiv” algoritmus így fest:

[MszT – megszámolás tétel alkalmazása:]
dbT:=0
Ciklus I=1-től N-ig
Ha T(X(I)) akkor dbT:+1
Ciklus vége
Ha dbT¹0 akkor
[ST – sorozatszámítás tétel alkalmazása:]
össz:=0
Ciklus I=1-től N-ig
össz:=össz+c(T(X(I)))*X(I)
Ciklus vége
átl:=össz/dbT
különben
átl:=0
Elágazás vége

5. lépés: az algoritmus „naivitásának” megszüntetése –Uf”-höz–:

Mindenek előtt a sorozatszámítás ciklusmagjára fókuszáljunk. Ebben az alábbi módon kiszámolható függvény szerepel, egy kifejezés részeként.

Függvény c(Konstans x:Logikai): Egész
Ha x akkor c:=1
különben c:=0
Függvény vége.

Az értékadást a PT1 fordított alkalmazásával: (egy segédváltozó bevezetésével) két értékadásra bontjuk:

SS:=c(T(X(I)))
össz:=össz+SS*X(I)

Világos, hogy megengedett a függvény hívása helyett magát a törzsét a hívás helyére beilleszteni –az aktuális paraméterekkel (mind a bemeneti, mind az érték paraméterre gondolva)–:

Ha T(X(I)) akkor SS:=1
különben SS:=0
össz:=össz+SS*X(I)

A PT17 „fordított” alkalmazásával az S-re vonatkozó értékadást bevisszük az elágazás mindkét ágába:

Ha T(X(I)) akkor SS:=1; össz:=össz+SS*X(I)
különben SS:=0; össz:=össz+SS*X(I)

A PT1-gyel az értékadás az SS segédváltozót kiküszöböljük:

Ha T(X(I)) akkor össz:=össz+1*X(I)
különben össz:=össz+0*X(I)

A „nem transzformáló” különben-ágat elhagyva a teljes algoritmus így áll elő:

[MszT – megszámolás tétel alkalmazása:]
dbT:=0
Ciklus I=1-től N-ig
Ha T(X(I)) akkor dbT:+1
Ciklus vége
Ha dbT¹0 akkor
[ST – sorozatszámítás tétel alkalmazása:]
össz:=0
Ciklus I=1-től N-ig
Ha T(X(I)) akkor össz:=össz+X(I)
Ciklus vége
átl:=össz/dbT
különben
átl:=0
Elágazás vége

A továbblépéshez most is a két tételt egymás közelségébe kell vinni. Ennek nincs akadálya, hiszen a dbT-től függetlenül elvégezhető az összegzés, legfeljebb „fölöslegesen” dolgozunk…

[MszT – megszámolás tétel alkalmazása:]
dbT:=0
Ciklus I=1-től N-ig
Ha T(X(I)) akkor dbT:+1
Ciklus vége
[ST – sorozatszámítás tétel alkalmazása:]
össz:=0
Ciklus I=1-től N-ig
Ha T(X(I)) akkor össz:=össz+X(I)
Ciklus vége
Ha dbT¹0 akkor
átl:=össz/dbT
különben
átl:=0
Elágazás vége

A PT10 ismételt alkalmazása után egyetlen ciklus végzi a két tétel lényegi részét. Majd a PT17 „fordított” alkalmazásával egyesítjük az elágazásokat:

dbT:=0; össz:=0
Ciklus I=1-től N-ig
Ha T(X(I)) akkor dbT:+1; össz:=össz+X(I)
Ciklus vége

Ezzel elértük a már korábban más úton levezetett algoritmust:

dbT:=0; össz:=0
Ciklus I=1-től N-ig
Ha T(X(I)) akkor dbT:+1; össz:=össz+X(I)
Ciklus vége
Ha dbT¹0 akkor
átl:=össz/dbT
különben
átl:=0
Elágazás vége

Gyakorlásként oldjuk meg a következő feladatot: számítsuk ki egy számsorozat pozitív és negatív elemeinek átlagát!

2. Megszámolással összeépítés

A megszámolást három elemi programozási tétellel érdemes egybeépíteni, az eldöntéssel, a kiválasztással, valamint a kereséssel.

Itt olyan kérdéseket tehetünk fel, hogy „van-e egy sorozatban legalább/legfeljebb/pontosan K db T tulajdonságú elem”, vagy hogy „adjuk meg a sorozat K. T tulajdonságú elemét” stb.

Az általánossága miatt nézzük a megszámolás és a keresés egymásra építését! Az eldöntésnél, illetve a kiválasztásnál hasonlóan kellene eljárnunk, hiszen e két típusalgoritmus megoldásszövege része a keresés megoldásszövegének.

1. lépés: a specifikáció elkészítése:

Be: NÎN, XÎH^*, KÎN, T:H®L

Ki: VANÎL, SORSZÎN

Ef: N=Hossz(X) Ù KÎ[1..N]

Uf: VAN=c(T(X_i))³K Ù
VAN Þ SORSZÎ[1..N] Ù T(X_SORSZ) Ù c(T(X_i))=K

2. lépés: az utófeltétel felbontása:

Uf Û VAN=($jÎ[1..N]: c(T(X_i))=K) Ù (1a)
VAN Þ SORSZÎ[1..N] Ù T(X_SORSZ) (1b)
Ù c(T(X_i))=K (2)

3. lépés: a felbontás helyességének belátása:

Valójában, ami egyáltalán belátandó:

c(T(X_i))³K Û $jÎ[1..N]: c(T(X_i))=K.

a K£N feltétel mellett.

(Þ): Ha az ekvivalencia bal oldala igaz, akkor

§ mivel c(T(x_i))=0 vagy 1, ezért a jobboldali formula "j: j<K-ra biztosan hamisak;

§ továbbá a szumma monoton növekedő az elemszám növekedtével;

§ és a legfeljebb „1-gyel növekedés” miatt a K értéket csak úgy lépheti túl, ha közben valamilyen j-re fel is veszi azt.

(Ü): Ha az ekvivalencia jobb oldala teljesül, akkor
mivel c(T(x_i))³0, ezért j=N-re nyilvánvalóan ³K teljesül.

4. lépés: a „naiv” algoritmus generálása:

Az (1a-b) a KT furcsa variánsának az utófeltétele. A (2) pedig az MszT utófeltételére emlékeztet (az ottani N-t és DB-t cserélve SORSZ-ra és K-ra).

Érdemes figyelmünket először a KT alkalmazására koncentrálni. A megoldás keretéül a KT maga szolgál. Ennek 3. paramétere –mint korábban láttuk– egy logikai értékű függvény, ahova jelen esetben az a reláció kerül, amely egyik oldalán az MszT által –x_i-vel bezárólag– kiszámolt darabszám, a másikon pedig a K konstans van: Megszámolás(i,X,T)³K. Az MszT a keresésben való továbblépéssel egyre bővülő sorozatra (x₁,...,x_i) vonatkozik:

(Van,SORSZ):=Keresés(N,X,iÎ[1..N]: Megszámolás(i,X,T)³K)

szolgáltatja az alábbi megoldást:

Eljárás MegszámolvaKeres(Be: N:PozEgész,X:Tömb(1..N:H_elemTíp):
Ki: VAN:Logikai, SORSZ:PozEgész):

...
I:=1
Ciklus amíg I£N és nem Megszámol(I,X)³K
I:+1
Ciklus vége
VAN:=(I£N)
Ha VAN akkor SORSZ:=I
Eljárás vége.

ahol a Megszámol függvényt az MszT alapján algoritmizáljuk (2)-höz, amely kielégíti az alábbi utófeltételt:

Megszámol(j,X)= (3)

Függvény Megszámol(Be: J:NemNegEgész,X:Tömb(1..N:H_elemTíp)):
NemNegEgész

...
DB:=0
Ciklus m=1-től J-ig
Ha T(X(m)) akkor DB:+1
Ciklus vége
Megszámol:=DB
Függvény vége.

5. lépés: az algoritmus „naivitásának” megszüntetése:

Térjünk vissza a felsőbb szintű eljáráshoz! Az egyszerűsítést nagyban akadályozó azon tényt, hogy az MszT alkalmazása a ciklus feltételében fordul elő, a PT11 programtranszformációval szüntethetjük meg. (Célszerűségből segédváltozóként DB-t választottunk. Persze tudva arról, hogy ezzel a döntésünkkel kifejezett interferenciát okozhatunk a már meglévő program részekkel. Mivel DB funkciójának megfelelő szerepet kap, ez kellő garancia arra, hogy az „áthallás” nem megy a program megbízhatóságának rovására.) Ezután kapjuk:

...
I:=1; DB:=Megszámol(1,X)
Ciklus amíg I£N és nem DB³K
I:+1; DB:=Megszámol(I,X)
Ciklus vége
VAN:=(I£N)
Ha VAN akkor SORSZ:=I
...

A PT12 programtranszformációval megspórolhatjuk a többszörös Megszámol függvényhívást.

Most az

§ x:=e helyett I:=1; DB:=Megszámol(1,X)[SzP5]
de tudva, hogy
előző(e) ezekre nem más, mint I:=0; DB=0

§ x:=Következő(x) helyett I:+1; DB:=Megszámol(I,X)

§ T(x) helyett nem DB³K

§ l helyett VAN

szerepel.

...
I:=0; DB:=0; VAN:=Hamis
Ciklus amíg I<N és nem VAN
I:+1; DB:=Megszámol(I,X)
VAN:=DB³K
Ciklus vége
Ha VAN akkor SORSZ:=I
...

A további ésszerűsítés már nem végezhető el egyszerűen valamilyen programtranszformáció segítségével. Mélyebb összefüggéseket kell keresnünk. E célból fogalmazzuk meg a felső szint ciklusának invariáns állítását. A keresés szokásos invariánsa:

"jÎ[1..i-1]: ØT(x_j)

ami a mostani esetre újrafogalmazva:

"jÎ[1..i-1]: ØMegszámol(j,X)³K

Figyelembe véve, hogy a ciklusmag mindössze I:+1, így a megragadandó állításban kapcsolatot kell találni a Megszámol(I,X) és a Megszámol(I+1,X) között.

Állítás:

Megszámol(i,X)=L Megszámol(i+1,X)=L Ú
Megszámol(i+1,X)=L+1

Bizonyítás:

Vizsgáljuk meg az állítás következményrészét:

Megszámol(i+1,X)=L Ú Megszámol(i+1,X)=L+1 (4)

A (3) és az c függvény értelmezése miatt

(4) Û (Megszámol(i,X)=L Ù ØT(x_i+1))
Ú (Megszámol(i,X)=L+1 Ù T(x_i+1))

Az állítás feltételét figyelembe véve ez ekvivalens az alábbival:

ØT(x_j+1) Ú T(x_j+1) Û Igaz.

(Qed.)

Az állítás fontos gyakorlati következménye, hogy az előző Megszámol(j,X) érték fölhasználható újraszámolás (azaz az eljárás újrahívása) nélkül is.

Nyilvánvaló az előbbi állítás, a (3) és az c függvény értelmezése alapján, hogy az alábbiak ekvivalens eredményre vezetnek (nagyon is eltérő hatékonyság mellett):

DB:=Megszámol(I,X) , ill. Ha T(X(I)) akkor DB:+1

Így jutunk a végső változathoz:

...
I:=0; DB:=0; VAN:=Igaz
Ciklus amíg I<N és VAN
I:+1
Ha T(X(I)) akkor DB:+1
VAN:=nem DB³K
Ciklus vége
Ha VAN akkor SORSZ:=I
...

3. Maximum-kiválasztással összeépítés

Maximum-kiválasztással kapcsolatban efféle kérdéseket fogalmazhatunk meg: 1) hány darab maximális értékű elem van, 2) melyek a maximális értékű elemek, 3) van-e több maximális értékű elem.

Ezeknél a maximum-kiválasztást kell egybeépíteni a megszámolással, a kiválogatással, illetve az eldöntéssel.

Mivel a kigyűjtéses kiválogatás mindig tartalmaz egy megszámolást, így csak a kiválogatással kell foglalkoznunk.

… hf …

Emlékeztető …

... a 2. feladatsor 1. feladatának utófeltételére, amelyben kiválóan látszanak az alkalmazandó programozási tételek:

A feladat:

Megmértük N alkalommal a felszín tengerszint fölötti magasságát. Feltételezésünk szerint ott van víz, ahol a mért érték 0, és ott van szárazföld, ahol a mért érték >0. A méréssorozatot szárazföld fölött kezdtük és fejeztük be. Adjuk meg a mért szakaszon a szigetek kezdeteit és végeit!

Megoldás:

Specifikáció:

Be: NÎN, MagasságÎR^*

Ki: DbÎN, SzigetÎ(Kezdet´Vég)^*, Kezdet,Vég=N

Ef: N=Hossz(Magasság) Ù
Magasság₁,Magasság_N>0 Ù "iÎ(1..N):Magasság_i³0

Uf: Ù "iÎ[1..Első):X_i>0 Ù "iÎ(Utolsó..N]:X_i>0
Ù SzigetÎ([1..N]x[1..N])^Db Ù HalmazFelsorolás(Sziget)
Ù "iÎ[1..Db]: "jÎ[Sziget_i.kezdet,Sziget_i.vég]: Magasság_j>0
Ù SzigetKezdet(Sziget_i.kezdet) Ù SzigetVég(Sziget_i.vég)

Def:	SzigetKezdet: L®L	SzigetVég: N®L
	SzigetKezdet(i):=Magassági>0 és Magassági–1=0	SzigetVég(i):=Magassági>0 és Magassági+1=0

---

^[1] … amint olvashatjuk a „Programozási tételek szerepe a gyakorlati programozásban” c. anyagban…

^[2] Szándékosan nincs jelölve a paraméter hozzáférési joga, ugyanis megengedjük –az egyébként nem túl „tisztességes”– a paraméter megváltozását.

^[3] azaz valamely paraméter a függvény kiértékelése során megváltozna

^[4] … vagy „suttyomban” valamely globális adatot megváltoztató…

^[5] Gondolja meg: mi történik, ha G(x,y) nem x-invariáns?

^[6] Nyilvánvaló tulajdonságokkal:

$Előző(x) Þ Előző(x)<x Ù Következő(Előző(x))=x

$Következő(x) Þ x<Következő(x) Ù Előző(Következő(x))=x

^[7] Itt most a korábbiaknál „precízebb” ez a szignatúra: még a sorozathosszakat is tartalmazza.

^[8] Talán szokatlan módon a paraméterlistán a bemeneti célra szolgáló paramétert nem a ’Konstans’ minősítővel vezetjük be, hanem a ’Be:’-vel, a kimeneti célra szolgálót nem Változó-ként, hanem ’Ki:’-ként aposztrofáljuk; így mód van az információt ki és bevivőre a ’BeKi:’-vel ezt a kétirányúságot is kifejezni.

^[9] A továbbiakban is közvetlen (anonim) típusdeklarációt alkalmazunk, amely slampos ugyan, de most céljainknak megfelelő.

^[10] Ezt a c függvényt a későbbiekben is fölhasználjuk, de már definiálás nélkül.

---

[SzP1]Hogy éppen ezt választottuk aszimmetrikusnak s nem a másikat, annak az az oka, hogy visszamenőleg nem akartuk a tételek algoritmusait módosítani.

[SzP2]Értsd: ekvivalens működését…

[SzP3]Emlékeztetőül az y-invarianciáról: Egy f: X´Y®Z, f(x,y) leképezést megvalósító F(x,y) függvényeljárást y-invariánsnak (második változó szerint invariánsnak) nevezünk, ha "(x,y)ÎDom_f: y'=y.

[SzP4]
Mellékhatásnak véve akár a hiba miatti programelszállást is!

[SzP5]Mintha az absztrakt algoritmus x-e helyébe az (I,DB) pár kerülne.