ProgramozásMódszertan
3. előadás’2001
(vázlat)

1.      Pascal kódolási szabályok

1.1. Miről is van szó?

·        A kódolás minél mechanikusabb tétele.

·        Csak a nyelv meghatározta dolgokra koncentrálás.

·        „Csak” a felhasználóval való zavartalan kommunikáció megszervezése.

Megjegyzés: a programok legtöbbjénél ez viszi el a kód 95%-át. Tehát nem arról van szó, hogy bagatellizálni kell e programozási lépést, hanem csak azt, hogy a feladat lényegét nem a kódolás során kell megoldani (hanem előbb).

·        A kódolási szabályok az adott programozási nyelven nyugszanak, tehát egyediek.

1.2. A Turbo Pascal kódolási szabályok

Az alábbiakban nem törekszünk teljességre. A lényeg és az „izgalmasabb” részletek bemu­tatása a cél. S mintául szolgáljanak más programozási nyelvek kódolási szabályainak meg­tervezéséhez.

Algoritmikus szerkezet

Pascal-szerkezet
Típusdefiníció

Konstans
  MaxN:Egész(100)
Típus
  TMag=Tömb(1..MaxN:TElem)
  TDátum=Rekord(év,hó,nap:Egész)

Const
  MaxN=100;
Type
  TMag=Array[1..MaxN] of TElem;
  TDatum=Record
         ev,ho,nap:Word
        End;
Típusdeklaráció

Változó
  Db,i:Egész
Konstans
  ma:TDátum(év:2001,hó:10,nap:1)
  mag:TMag

Var
  Db,i:Integer;
Const
  ma:TDatum=(ev:2001;ho:10;nap:1);
  mag:TMag;
Értékadás

x:=kif

x:=kif;
Alprogramhívás

Beolvasás(Db,mag)

Beolvasas(Db,mag);
Beolvasás

Be: Db [0£Db£MaxN]






Be: mag(1..Db) [mag(i)>0]

Repeat
 {$i-}
 Write(’Mi a szösz:’);
 Readln(Db);
 {$i+}
Until (IOResult=0) and
      (Db>=0) and (Db<=MaxN);

For i:=1 to N do
Begin
 Writeln(’Mi a szösz tömb ez.’);
 Repeat
  {$i-}
  Write(i:3,’. elem:’);
  Readln(mag[i]);
  {$i+}
 Until (IOResult=0) and
      (mag[i]>0);
End;
…

…

…

2.      Specifikáció – Algoritmus – Kód

2.1. Kapcsolatok

[ Adatszerkezet Þ Alg.TipDef ]

Spec.Be + Spec.Ki Þ Alg.TipDef
Spec.Be + Spec.Ki + Alg.TipDef Þ Alg.TipDekl

Spec.Ef Þ [Alg.Be Þ] Kód.Beolv

Spec.Uf Þ Alg.Végrehajt Þ Kód.Végrehajt

Spec.Def Þ Alg.Elj/Fv Þ Kód.Elj/Fv

2.2. Egy korábbi feladatpélda:

Specifikáció:

Bemenet:     NÎN, HallgatókÎ(Név´Szak´Évfolyam)*,
Név= S, Szak={Info, Mat, Fiz, …[1]}, Évfolyam=N

Kimenet:      VaneÎL

Előfeltétel:   "iÎ[1..N]: Hallgatóki.Név¹’’ Ù Hallgatóki.ÉvfolyamÎ[1..5]

Utófeltétel:   Vane = $iÎ[1..N]: Hallgatóki.Szak=Info Ù Hallgatóki.Évfolyam=1

Adatszerkezet: Tömb Þ Alg.TipDef :

Konstans MaxN:Egész(100)

Spec.Be + Spec.Ki Þ Alg.TipDef :

Típus   TNév=Szöveg
        TSzak=(Info, Mat, Fiz, …)
        TÉvfolyam=Egész
        THallgatók:Rekord(
                     Név:TNév
                     Szak:TSzak
                     Évfolyam:TÉvfolyam)
        THallgatók=Tömb(1..MaxN:THallgató)

Spec.Be + Spec.Ki + Alg.TipDef Þ Alg.TipDekl :

Változó N:Egész
        Hallgatók:THallgatók
        Vane:Logikai

Spec.Ef Þ [Alg.Be Þ] Kód.Beolv

Be: N
Be: Hallgató(1..N)
  [Hallgató(i).Név¹’’ és
   Hallgató(i).ÉvfolyamÎ[1..5]]

l. előbb

Spec.Uf Þ Alg.Végrehajt Þ Kód.Végrehajt

…

3.      Mit jelent a tétel bizonyítás

Figyeljük meg például a Kiválasztás tétel bizonyítását!

Specifikáció:

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

Ki:      SorszÎN

Ef:       Hossz(X)=N Ù $iÎ[1..N] : T(xi)

Uf:       SorszÎ[1..N]  Ù  T(xSorsz)

Alg:

Konstans MaxN:Egész(???)
Típus THk=Tömb(1..MaxN:TH)

Eljárás Kiválasztás(Konstans N:Egész, X:THk
                    Változó  Sorsz:Egész):
  Változó
    i:Egész

  i:=1
  Ciklus amíg nem T(X(i))
    i:+1
  Ciklus vége
  Sorsz:=i
Eljárás vége.

3.1. A bizonyítás ötlete

A helyes program mint állapottér-transzformáció az Ef által behatárolt részállapotból indul ki, és utasításról utasításra haladva transzformálja az állapottér egyes komponenseit mind­addig, amíg az Uf által meghatározott végállapotba nem jut.

Kövessük tehát mi is utasításról utasításra az állapottér transzformált részállapot-halmazait! Vagyis adjuk meg a predikátumokat az egyes utasítások mögött kiindulva az Ef-ből. Ha elju­tottunk az Uf-be, akkor a bizonyítás kész.

3.2. Az „egyenes” bizonyítás lehetetlensége

1.      Egy feladat specifikációjában az Ef-t tetszőlegesen szűkíthetjük, a korábbi megoldás meg­oldás marad ezután is.

Például, Ef: … $iÎ[1..N Div 2] : T(x2*i) – azaz létezik páros indexű T-tulajdonságú

2.      Az Ef-nek semmi látható közölni valója nincs a feladatról. Már csak azért is igaz ez a ki­jelentés, mert a tételek között soknak ugyanaz (a „semmi”, azaz AZONOSAN IGAZ) az Ef-e.

3.3. A bizonyítás támpontjai

A legtöbb mondanivalója a feladatról az Uf-nek van. Ebből kell tehát kiindulni, s követni visszafelé a „transzformáció-inverzének” a működését, amíg az Ef-hez el nem érünk.

A transzformáció utáni állapotból az utasítás előttire következtetni nem mindig könnyű, ezért segédállításokat (és rajtuk nyugvó következtetési szabályokat) kell találni.

A pontos részletek mellőzésével élvezzük a levezetés báját/lényegét.

3.4. Menet

Az algoritmus tevékenység részére figyelnünk csak. A megfelelő helyekre beillesztjük az újabb állításokat.

0.

[f4]
 i:=1
[f3]
 Ciklus [f2] amíg nem T(X(i))
   i:+1
 Ciklus vége
[f1]
 Sorsz:=i
[Uf]

Uf: SorszÎ[1..N]  Ù  T(xSorsz)

1.

[f4]
 i:=1
[f3]
 Ciklus [f2] amíg nem T(X(i))
   i:+1
 Ciklus vége
[f1]
 Sorsz:=i
[SorszÎ[1..N]  Ù  T(xSorsz)]

f1: iÎ[1..N]  Ù  T(xi)

2.

[f4]
 i:=1
[f3]
 Ciklus [f2] amíg nem T(X(i))
   i:+1
 Ciklus vége
[iÎ[1..N]  Ù  T(xi)]
 Sorsz:=i
[SorszÎ[1..N]  Ù  T(xSorsz)]

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

1. Állítás: ha f2 egyszer igaz, akkor igaz is marad a ciklus végrehajtása során.

Ui.: (Kövessük a ciklus egyszeri végre­hajtását.)

     Tfh. f2(i) Þ (
     (ØT(xi) ◄i:+1►[2] f2(i-1) Ù ØT(xi-1))º
      "jÎ[1..i-2]: ØT(xj)  Ù  ØT(xi-1)ºf2(i))
     (T(xi) ◄nul► f2(i)[3])

3.

[f4]
 i:=1
[f3]
 Ciklus ["jÎ[1..i-1]: ØT(xj)]
        amíg nem T(X(i))
   i:+1
 Ciklus vége
[iÎ[1..N]  Ù  T(xi)]
 Sorsz:=i
[SorszÎ[1..N]  Ù  T(xSorsz)]

f3(i): "jÎ[1..i-1]: ØT(xj)ºf2(i)

2. Állítás: f3  igaz.

Ui.: Igaz◄i:=1► f3(1) º
            º"jÎ[1..1-1]: ØT(xj)ºIgaz

3. Állítás: f2 kezdetben (i=1 esetén) igaz.

Ui.: 2. állítás következménye.

Állítás: f2 invariáns állítás.

Ui.: 1. és 3. állítás következménye.

(Azaz betöltheti a ciklusinvariáns szere­pét.)

4.

[f4]
 i:=1
[Igaz]
 Ciklus ["jÎ[1..i-1]: ØT(xj)]
        amíg nem T(X(i))
   i:+1
 Ciklus vége
[iÎ[1..N]  Ù  T(xi)]
 Sorsz:=i
[SorszÎ[1..N]  Ù  T(xSorsz)]

f4: Igaz

5.

[Igaz]
 i:=1
[Igaz]
 Ciklus ["jÎ[1..i-1]: ØT(xj)]
        amíg nem T(X(i))
   i:+1
 Ciklus vége
[iÎ[1..N]  Ù  T(xi)]
 Sorsz:=i
[SorszÎ[1..N]  Ù  T(xSorsz)]

Ef. ???

Nem jött ki az Ef!?! Hol a hiba a gondolatmenetben?

Figyeljük meg, mi történik, ha az Ef nem teljesül a bemenő adatra! Válasz: a ciklusból nincs (legális) „menekvés”! Vagyis, amit kaptunk így fogalmazható meg: ha a program terminál (megáll, eljut egy „legális” végállapotba), akkor az Uf-nek megfelelő állapotban lesz.

Koncentráljunk mármost a legális megállásra! A megállásnak az a feltétele, hogy legyen olyan („absztrakt”) függvény, amivel a még hátralévő ciklus lépések számát le tudjuk írni, s igaz rá, hogy a ciklus minden lépése során éppen eggyel csökken.

[f4]
 i:=1
[f3]
 Ciklus [f2(i) Ù cl(i)>0]
        amíg nem T(X(i))
   i:+1
 Ciklus vége
[iÎ[1..N]  Ù  T(xi)]
 Sorsz:=i
[SorszÎ[1..N]  Ù  T(xSorsz)]

Az f2–t nem részleteztük, az f3 és f4 még nem ismert, cl a még hátralévő cikluslépések számát leíró függvény.

cl(i): K-i (KÎN rögzített konstans)

Állítás: $jÎ[1..N]: T(xj) Þ
            $KÎ[1..N]: cl(i)³0

Ui.: Legyen KÎ[1..N]: T(xK).

   Ekkor "jÎ[1..K-1]: cl(j)>0 Ù cl(K)=0.

Tehát:

f3: $jÎ[1..N]: T(xj)

[f4]
 i:=1
[$jÎ[1..N]: T(xj)]
 Ciklus [f2(i) Ù K-i>0]
        amíg nem T(X(i))
   i:+1
 Ciklus vége
[iÎ[1..N]  Ù  T(xi)]
 Sorsz:=i
[SorszÎ[1..N]  Ù  T(xSorsz)]

f4: f3

Állítás: f4◄i:=1►f3

Ui.: „$jÎ[1..N]: T(xj)” kifejezés független i-től, ezért az utasítás megtartja ennek igazságtartalmát.

E második gondolatsor végére megszületett az Ef is.

4.      További egyszerűbb Programozási tételek

4.1. Megszámolás tétel

Megszámolás(H*,F(H,L)):N

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

Ki:       DbÎN

Ef:       Hossz(X)=N

Uf:      

Def:     :L®{0,1}
             

Alg:

Konstans MaxN:Egész(???)
Típus THk=Tömb(1..MaxN:TH)

Eljárás Megszamolás(Konstans N:Egész, X:THk
                    Változó  Db:Egész):
  Változó
    i:Egé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.

Megjegyzések:

1.      Az itt felvetődő „elemszámlálásos” ötlet és formalizmus sokszor felhasználandó! A továbbiakban nem definiáljuk a khi-függvényt.

2.      Bevezettük a programozási nyelvekben is gyakorta meglevő „inkrementálás” (növelés) műveletet. Értelmezését az alábbi: példa érzékelteti:

x:+y  ugyanaz, mintha            x:=x+y

(Persze kitalálható a jelentése a dekrement és társai műveleteknek: x:-y, x:*y, x:/x )

3.      Érdemes eltűnődni a tételnek és a sorozatszámítás tétel (S-s változatának) nagyfokú hasonlóságán.

4.2. Maximumkiválasztás tétel

Maximumkiválasztás(H*,F(HxH,L)):N [4]  vagy  Maximumkiválasztás(H*,F(HxH,L)):H[5]

Be:      NÎN, XÎH*, £ÎF(HxH,L)

Ki:      MaxiÎN

Ef:       Hossz(X)=N Ù N³1 Ù RendezettHalmaz£(H)

Uf:       MaxiÎ[1..N]  Ù  "iÎ[1..N] : xMaxi³xi

Alg:

Konstans MaxN:Egész(???)
Típus THk=Tömb(1..MaxN:TH)

Eljárás Maximumkiválasztás(Konstans N:Egész, X:THk
                           Változó  Maxi:Egész):
  Változó
    i:Egész

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

Megjegyzések:

1.      Az algoritmusbeli >-reláció a specifikációbeli £ „értelemszerű” algoritmikus párja.

2.      Meggondolandó, milyen specifikációra „rimmelne” az az algoritmus, amelyben a > helyett ³-reláció szerepelne!

3.      Specifikálja a maximumkiválasztás másik változatát is!

4.3. Kiválogatás tétel

Kiválogatás(H*,F(H,L)):N* [6]   vagy  Kiválogatás (H*,H,F(H,L)):H* [7]

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

Ki:      DbÎN, YÎN*

Ef:       Hossz(X)=N

Uf:        Ù YÎ[1..N]Db  Ù  "iÎ[1..Db]: T(xyi) Ù  HalmazFölsorolás(Y)

Alg:

Konstans MaxN:Egész(???)
Típus THk=Tömb(1..MaxN:TH)
     TIndk=Tömb(1..MaxN:Egész)

Eljárás Kiválogatás(Konstans N:Egész, X:THk
                    Változó  Db:Egész, Y:TIndk):
  Változó
    i:Egész

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

 

Tartalom

1.     Pascal kódolási szabályok. 1

1.1. Miről is van szó?. 1

1.2. A Turbo Pascal kódolási szabályok. 1

2.     Specifikáció – Algoritmus – Kód. 2

2.1. Kapcsolatok. 2

2.2. Egy korábbi feladatpélda: 2

3.     Mit jelent a tétel bizonyítás. 3

3.1. A bizonyítás ötlete. 4

3.2. Az „egyenes” bizonyítás lehetetlensége. 4

3.3. A bizonyítás támpontjai 4

3.4. Menet 4

4.     További egyszerűbb Programozási tételek. 7

4.1. Megszámolás tétel 7

4.2. Maximumkiválasztás tétel 8

4.3. Kiválogatás tétel 8

 


[1] A „…” jelentése: itt egy felsorolás lenne, amit most nem folytatunk )formálisan persze kellene, mivel ki nem található)! Figyelem: így csak egy-szak rendelhető a hallgatóhoz! Nagy baj ez?

[2] „f1◄i:+1► f2” jelentése: „az f1–ből i:+1 utasítás végrehajtása után igaz f2”.

[3] Azaz nem változott a nul (üres) utasítás hatására.

[4] Maximális elem indexének kiválasztása.

[5] Maximális elem (értékének) kiválasztása.

[6] A T-tulajdonságúak indexeinek kiválogatása.

[7] A T-tulajdonságúak (értékeinek) kiválogatása.