Specifikáció A leggyengébb előfeltétel

Specifikáció

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˝orizheto˝ . Ezért bevezetünk néhány új fogalmat, majd ezek segítségével egy elégséges feltételt adunk a megoldásra.

˝ 5.1. A leggyengébb elofeltétel El˝oször a program futásának adjuk meg egy a programfüggvénynél kényelmesebben használható jellemzését.

"!$#&%('*),+.-0/2143 5 6 %78 "292:

˝ 16. DEFINÍCIÓ : L EGGYENGÉBB EL OFELTÉTEL program, állítás. Ekkor az program Legyen utófeltételhez tartozó leggyengébb el˝ofeltétele az az állítás, amelyre:

A leggyengébb el˝ofelté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˝ofeltétel igazsághalmazán kívül is lehetnek olyan pontok, amelybo˝ 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˝uködése úgy is jellemzhet˝o, hogy megadjuk a program tetsz˝oleges utófeltételhez tartozó leggyengébb el˝ofeltételét. A feladat megoldása során az a célunk, hogy olyan programot találjunk, amelyik bizonyos feltételeknek eleget tev˝o 45

46

5. SPECIFIKÁCIÓ

pontokban terminál. Ezért azt mondhatjuk, hogy ha a számunkra kedvez˝o végállapotokra megadjuk a program leggyengébb el˝ofeltételét, akkor a programfüggvény meghatározása nélkül jellemezzük a program m˝uködését. A most következ˝o tétel a leggyengébb el˝ofeltétel néhány fontos tulajdonságát mondja ki.

;;$<, program, =>$ 2?@ állítások. Ekkor (1) AB,CEDFG!HJAB ,CEDF , (2) Ha =EI , akkor L=KNM J L ! =K I L=OMP , , (3) L=KNQ J L I J =;QP . (4)

3. TÉTEL : A Legyen

TULAJDONSÁGAI

Az els˝o tulajdonságot a csoda kizárása elvének, a másodikat monotonitási tulajdonságnak nevezzük. Bizonyítás:

RS%T' U AT"CE D7 . Ekkor a leggyengébb el˝o%V'V),+W-X/F1 és 5 %SY AB"CED7Z[!]\ . Ez UJ =K `_ UJ L a . Ekkor %T'^),+W-X/F1 és 2. Indirekt: 5 %SK Tegyük =,bM(fel,5 hogy %S(RSc %^' d . Ez viszont ellentmond annak a feltételnek, mely szerint = K " 1. Indirekt: Tegyük fel, hogy feltétel definíciója szerint: nyilvánvaló ellentmondás.

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

UJ L a UJ =K

5

d =,

5.1. ábra. A leggyengébb el˝ofeltétel és a metszet kapcsolata (a)

L=KNM J L I J =;MP , ui.: U L=fgM a . Ekkor %h' L=Ka és %e' , Legyen %e' azaz 5 %7 i " . Ekkor azonban 5 %h%7i'h ),+W -X= /F1késj 5 ", ! %S` =O MP=," ,,illetve azaz %e' L=lM*a .

47

5.2. A FELADAT SPECIFIKÁCIÓJA

(b)

J =;MPI L=fNM J L , ui.: L=?MB . Ekkor a leggyengébb el˝ofeltétel definíciója Legyen %m' =nM +.-0/21 és 5 %Sp =o MY" . Felhasználva, alapján %n'o), hogy "q! =, ij " , adódik, =, és 5 %S " , azaz hogy 5 G %SK %h' L=Ka és %e' UJ L , tehát %e' UJ =KNM . 5

L=Ka

" =,

5.2. ábra. A leggyengébb el˝ofeltétel és az unió kapcsolata

%eU' UJ =KFQ h% ' L=f U a %h' L=f

%e' U L=f e% ' UU J a . %e' =hQ %h' L=lQP a

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

5.2. A feladat specifikációja A következ˝okben bevezetjük a feladat megadásának egy másik módját, és kimondunk egy a gyakorlat szempontjából nagyon fontos tételt. Általában a feladat nem függ az állapottér összes komponensét o˝ l, azaz az állapottér több pontjához is ugyanazt rendeli. Ezeket a pontokat fogjuk össze egy ponttá a paramétertér segítségével.

ro[$< rt rZu

s r tv E <se rwu Vs
17. DEFINÍCIÓ : PARAMÉTERTÉR Legyen feladat. A halmazt a feladat paraméterterének nevezzük, ha van olyan és reláció, hogy

Fontos észrevenni, hogy paraméterteret mindig lehet találni. Például maga a feladat állapottere minden esetben választható paramétertérnek úgy, hogy a definícióban

48

5. SPECIFIKÁCIÓ

rt

ru

r

szerepl˝o relációnak az identikus leképezést, -nek pedig magát az feladatot választjuk. Ám az, hogy egy konkrét esetben mit is választunk paramétertérnek a feladattól függ. Általában úgy választjuk meg a paraméterteret, hogy a következ˝o tételt kényelmesen tudjuk használni.

rn;Pk s r r t lPks r u Osk , r$!yr u 8x r t : z"'Ps =K{|}! #.%('<~3 % z8'Pr t 9,![r t -U t 1 z ,{|}! #.%('
4. TÉTEL : S PECIFIKÁCIÓ TÉTELE Legyen feladat, az egy paramétertere, , Legyen , és definiáljuk a következ˝o állításokat:

feladatot.

Bizonyítás: A megoldás definíciója két pontjának teljesülését kell belátnunk: 1.

)KlY),+W-X/F1 , ui. Legyen %e'*)K tetsz˝oleges. Ekkor az rt és rwu relációk definíciója miatt Rz"'sV %e' = { 2:

e% ' =f{aK UJ L,{ f)"+W-X/F1: 2. N%e'*); 5 %SÒr %S , ui. Legyen %*'<)K tetsz˝olegesen rögzített, z,'Bs olyan, amelyre %P' = { . Ekkor a feltétel szerint: 5 %S` {|,!yr u z8lr u r t %Sgk!yr %7: De ekkor a tétel feltétele alapján:

Vegyük észre, hogy a tétel feltételrendszerében használt jelölések felhasználhatók a feladat egy más módon történo˝ leírására. Ha a feldatot úgy definiáljuk, hogy megadjuk az állapotterét ( ), a paraméterterét ( ), valamint az el˝o- és utófeltételét ( illetve ) a paramétertér egy tetsz˝oleges pontjára, akkor azt mondjuk, hogy a feladatot specifikáljuk. Paramétertérnek általában az állapottér egy alterét szoktuk választani. Azokat a komponenseket válogatjuk ki, amelyek értékét˝ol függ, hogy a feladat mit rendel, amik paraméterezik a feladatot. A specifikáció tétele csak elégséges feltétel a megoldásra, azaz nem megfordítható: lehet adni olyan feladat-program párt, ahol a program megoldja a feladatot, de a specifikáció tétele nem teljesül. Ez természetesen attól is függ, hogy a feladatot hogyan specifikáljuk, azaz milyen paraméterteret választunk, és hogyan bontjuk a feladatot és relációk kompozíciójára.

ru

s

=

rt

49

5.3. A VÁLTOZÓ FOGALMA

5.3. A változó fogalma Az eddig elmondottakból alapján a specifikáció tétele még nem lenne hatékonyan használható, hiszen a paramétertér minden pontjára ellen˝oriznünk kellene a feltételek teljesülését. Ezért bevezetjük a változó fogalmát, aminek segítségével a feltételrendszer teljesülése egyszeru˝ en ellen˝orizheto˝ vé válik.

E! t p4<"

18. DEFINÍCIÓ : VÁLTOZÓ Az állapottér vényeit változóknak nevezzük.

8 $" egydimenziós projekciós függ-

A változók használatával egyszeru˝ síthetjük az állapottéren értelmezett állítások (el˝o- és utófeltételek, leggyengébb el˝ofeltétel) és relációk (programfüggvény) leírását. Mivel minden változó értelmezési tartománya az állapottér, és értékkészlete egy típusértékhalmaz, egy változót jellemezhetünk egy típussal, azaz beszélhetünk a változó típusáról. Ha a paramétertér is direktszorzat alakú – márpedig ez gyakran így van, ugyanis általában az állapottér egy altere – akkor a paramétertér egydimenziós projekciós függvényeit paraméterváltozóknak nevezzük. Az állapottér illetve a paramétertér egyes komponenseihez tartozó vátozókat illetve paraméterváltozókat az adott komponens alá írjuk. Tekintsünk egy egyszeru˝ példát: határozzuk meg két egész szám maximumát!

! E s! S

Az els˝o sor tehát azt jelenti, hogy az állapottér három egész komponensb o˝ l áll, melyeknek változói rendre , és . Hasonlóan a második sor jelentése: a paramétertér két egész komponensb o˝ l áll, az els˝o komponens változója , a másodiké . A paramétertér egy tetsz˝oleges eleméhez tartozó el˝o- és utófeltétel az állapottér egy tetsz˝oleges pontjában:

z % =& - { 1 ¡ ¢ - { 1 %S! S% k! z£M " - { 1 ¡ ¢ - { 1 %S! %S`¤ z £M

%7! %S8¤

S

zg zNM S% ! z NQ S% ! z g

A fenti jelölést tovább szoktuk egyszeru˝ síteni: mivel az állapottér változói és a paraméterváltozók mindenütt azonos argumentummal szerepelnek, az argumentumot – hiszen az nyilvánvaló – nem írjuk ki:

= 4 U¡ ¢ ! ! 4U¡ ¢ ! ¤

M M

! ¤ M ! Q ! g

A jelölés tovább egyszeru˝ síthet˝o! Mivel ezek a feltételek a paramétertér pontjaihoz tartoznak, nyilvánvaló, hogy a paraméterváltozók értékeit˝ol függnek. Ha nyilvánvaló, akkor az állítások indexe el is hagyható. A feladat specifikációja tehát:

50

5. SPECIFIKÁCIÓ

! E s@!¥¦ V7 =~ ! M ! ¤ M ¤

S M ! Q ! S A változók segítségével könnyen felírhatunk olyan függvényeket, amelyek az állapottér komponensein vannak értelmezve. Ha nem okoz félreértést, akkor az x 0bizonyos § :4:: X¨ jelölés helyett az § 4::4:g 0¨ jelölést használjuk.

A kés˝obbiekben bevezetünk majd olyan eszközöket, amelyek segítségével a feladat specifikációjából kiindulva olyan programokat készíthetünk, amelyek megoldják a feladatot.

5.4. A típusspecifikáció tétele A típusspecifikáció és a típus fogalmának bevezetésével tulajdonképpen a feladat fogalmát általánosítottuk, míg a megfeleltetés a megoldás fogalmának volt egyfajta általánosítása. Az imént megismert specifikáció tétele a megoldásra adott elégséges feltételt. Próbáljunk most a -n keresztüli megoldásra egy hasonló feltételt adni!

©

ª«m! U ¬ L D«&| ª®! ©FLD¯L°w 4 © D.±! D«L rV' r s =K{ { ;'P° r = ²{ }! ³=K{£xG´µ "²{ }! ,{wxG´ ahol ´ a program és a feladat állapottere közötti, a © -n keresztüli defi megoldás níciójában szerepl˝o leképezés. Ekkor ha Nzd's F= ²{ I ²{ akkor az program a © -n keresztül megoldja az r feladatot. Bizonyítás: A © -n keresztüli megoldás definíciója két pontjának teljesülését kell belátnunk: 1. ) Y) +W-X/F1 ¶·²¸0¹ §º , ui. ² ¶ & Legyen %e'*) . Ekkor Rz"'PsV 2%e' =K{| . Mivel © D.! D« , ´ -U t 1 %7 !yc \iMh´ - t 1 %S8 = ²{ F: UJ L"²{ : Felhasználva, hogy = ²{ K ´ -U t 1 %78;),+W-X/F1M±5 ´ - t 1 %Sg` ²{ 2:

5. TÉTEL : T ÍPUSPECIFIKÁCIÓ TÉTELE Legyen és adott típusspecifikáció és típus, és tegyük fel, hogy a reprezentáció helyes, azaz . Legyen továbbá , az állapottere , egy paramétertere , el˝o és utófeltétele pedig és . Legyen és tegyük fel, hogy állapottere illeszkedik állapotteréhez. Definiáljuk a következ˝o állításokat:

5.4. A TÍPUSSPECIFIKÁCIÓ TÉTELE

51

,²{ ,! {£xG´ ,

5 ´ -U t 1 %SgiY) ² tehát %h'h) ²¶ +W-X/F1 ¶·²¸X¹ §º : -U t 1 Or %S , ui. 2. »%('P)K ´>¼5 w¼p´ Legyen %E'n)K . A bizonyítás els˝o részében leírt lépéseket folytatva: mivel 5 G ´ -U t 1 %7` { xG´ , ´ 5 ´ - t 1 %Sggi { Klr %S: Mivel

Az, hogy a fenti tétel feltételei között kikötöttük, hogy a program állapottere illeszkedik a feladat állapotteréhez tulajdonképpen elhagyható. Ekkor a tétel a feladat és a program olyan kiterjesztéseire mondható ki, amelyek állapotterei illeszkednek egymáshoz (pontosan úgy, ahogy a megfeleltetést definiáltuk nem illeszked˝o állapotterek között). A következ˝o példában megmutatjuk, hogy -t gyenge igazsáhalmaz helyett er˝os igazsághalmazzal definiálnánk, akkor a tétel nem lenne igaz. , , , . Legyen állapottere Legyen és a paramétertér is legyen ugyanez: . Legyen specifikációja:

= ²{ ª « ! ¬ D « |¯ ¬ !¦#2½2L¾S9 D « !"¿ ¬ V!¦#.rq9 r ¬ H! s~! r = t }! #F½92 t }! #W¾79 = u }! \ u }! #F½9 #2½9 és r ½&(!@#W¾79 . Legyen Ekkor )Ko!¥ továbbá az elemi értékek halmaza À! #.% z&9 , ª! ©7D°Z , »ÁY'PÀ D ÁG! 3 Á`3!½& , és © az egy hosszú sorozatokra: © gÂ %SÃgG!$© Â zÃG!#F½ ¾792: Tegyük fel, hogy °!#.89 , oÀ±q ÀqLL , és rendelje az állapottere minden pontjához az önmagából álló egy hosszú sorozatot. Ennek a programnak az állapottere illeszkedik a fenti feladat állapotteréhez, és ´P!$© . Ekkor =ftxG´"!H\ és =uGxG´,!y\ tehát = t xG´ I t xGŃ = t xG´ I t xGŃ Az viszont könnyen látható, hogy ´>¼B5 G·¼p´ -U t 1 ½.!E#F½ ¾79q;c r ½.!E#W¾79 tehát a típus nem felel meg a specifikációnak.

52

5. SPECIFIKÁCIÓ

5.5. Példák

~!V#&ÄTÅ.%FÆ 6 s±%FÇ4È· CEÉ %FÊ.ÆËGÌ 6 ÆÍÉWÅFs Ê.É.Î9 , HnB m!E#ÏÄTÅ.%FÆ 6 ÂÂ ÄTÅ.%FÆ 6 s±6 %F Ç4ÈÃ s±%7Ç È ÂÂ sf%7Ç È£LCEÉ %FÊ&Æg6Ã sf%76 Ç È Â sf%76 Ç È£ËGÌ Æs Ê.É.Î£ÃÐCEÉ %FÊ.ÆÑ Â CEÉ %FÊ.Æ Ä^Å.%2Æ Ã ËÌ Æ Â ËÌ Æs ÊWÉ.Î£Ã 6 ÍÉWÅ ÍÉWÅFLCEÉ %2Ê.ÆgÃ s ÊWÉ.Î s ÊWÉ.Îs±%7ÇÈ·LËÌ ÆgÃ9 Legyen továbbá az H¥ állítás: '<$ ; G! zeneszerzo˝ . Mi lesz a fenti program -hez tartozó leggyengébb el˝ofeltétele? Megoldás: Írjuk fel el˝oször a program programfüggvényét: 5 G!E# Ä^Å.%2 Æ 6 Lsf%7ÇÈ 6 sf%76 Ç È£LCE É %2Ê.Æg s±%FÇ4È·Ls ÊWÉ.Î£ sCE É Ê.É.%FÎÊ.LÆËÄTÌ 6 Å. %FÆg Æ 9 ËÌ ÆLs ÊWÉ.Î£ ÍÉWÅFLCEÉ %FÊ.Æg EzekUután, el˝ofeltétel definícióját felhasználva: a aleggyengébb ,!#&Ä^Å.%2Æ 6 LÍÉWÅ2Ls ÊWÉ.Î9 , ui. 5 ÄT Å.%FÆ 6 Ò! #&s±%7Ç ÈN9 " ! #.CE6É %FÊ.Æ 9 " 5 5 s ÍÊWÉ.ÉWÎ£Å.Ó ! #&ËGÌ Æ 9 " 5 G s± %7ÇÈ! #.CEÉ %F6 Ê.Æs ÊWÉ.Î9(c " 5 CE É %F6 Ê&Æg! #&Ä^ Å.%2Æ 9qc " 5 ËGÌ ÆgÑ! #&s Ê.É.Î9(c " 2. A t LA u 7 . Igaz-e, hogy ha minden O[$ L programra példa: AetGLegyen ! A>u4 , akkor Aet ,! A>u ? 1. példa: Legyen program.

Megoldás: Felhasználva, hogy a leggyengébb el˝ofeltételek minden programra megegyeznek, egy alkalmas program választásával a válasz egyszeru˝ en megadható: rendelje az program az állapottér minden eleméhez az önmagából álló egy hosszúságú sorozatot. Ekkor könnyen látható, hogy tetsz˝oleges utófeltétel esetén:

Ekkor viszont

J L !Hq:

Aetb! Aet! A>uk![A>u

tehát a két feltétel megegyezik.

H![O*ÏrnlE< r$!# g LÔ LÔ gi3Ô !yÔM ! MPÔ¯ 9

3. példa: Specifikáljuk a következ˝o feladatot:

,

53

5.6. FELADATOK

Megoldás:

!VÕ ? s!@Ö oS =n ! M S! 7 S ! M NM ! 4. példa: Legyen r¦p , L program, s egy tetsz˝oleges halmaz. Legyenek továbbá r t $nTs és r u sB olyan relációk, hogy r!nr u xbr t , valamint Nzd'<s : .= × { }! r t t z ,{g}! r u z: × {g , akkor megoldja r -et? Igaz-e, hogy ha Nzd'<sV =K{GI Megoldás: Próbáljuk meg a megoldás definíciója két pontját belátni. Legyen %e'P) . Be kellene látnunk, hogy %e'*)"+W-X/F1 . Nézzük meg a specifikáció tételének bizonyítását: × ott felhasználtuk, hogy ekkor van olyan ze'Os , hogy %Y' = { . Igaz ez a = { -re is? × Sajnos – mivel = { -t o˝ sképpel definiáltuk, ez nem feltétlenül van így. Próbáljunk a fenti gondolatmenet alapján ellenpéldát adni: Legyen !Õ#F½9 , s!Õ#F½ ¾79 , r!Ø# ½2½. 9 , rte!Õ# ½½. ½ ¾9 , rZuh!Õ# ¾½&9 . × 6 × 6 Ekkor =fti!HÈ¯%FÙPÌ és =Kud!HÈ%FÙ*Ì , tehát az állítás feltételei teljesülnek függetlenül a programtól (ui. “hamisból minden következik"). Válasszuk most az alábbi programot: !~# ½2Ú$½4½4:Û:X:Üd9 . Ez a program nem megoldása a feladatnak, de teljesülnek rá is az állítás feltételei. Tehát az állítás nem igaz.

5.6. Feladatok 1. Legyen

= 2H@ Ìk'Ý . Igaz-e, ha »Ì'<ÝH =£I¦=XÞ t

tetsz˝oleges állapottér,

RSÎ'<Ý? L=K7G! J R7Î'<ÝH =gß £t&L K! NuW , akkor £t8à^·uK! wt&Q 2. Igaz-e, ha ·uhogy ? UJ t gá # 9Wga,â ' U u gá # 9Wg , akkor 3. Igaz-e, ha 'Tn ' )"+W-X/ § 1!l),+W-X/WãL1 ? t LATf! 4. t u Vp, programok. Igaz-e, ha »Aä Ñ esetén u A^ , akkor t ekvivalens u -vel? akkor

54

5. SPECIFIKÁCIÓ

!yå8å^G állapottér å!$#2½2L¾æS9W és a s~!yå`å r t és r u feladatok. r t !$# % t L% u z t z u Ôg83&Ô>! % t ÜO% u 9F

5. Adott az továbbá az

paramétertér,

r u specifikációja pedig: ! åÒåÑ? %t %u s@! åÒ å %t %u =n % t ![ % t MP % u !y% u ~ =OM ! % t ÜO% u g Azonosak-e az r t és r u feladatok? 6. Tekintsük az alábbi két feladatot: rt specifikációja: ! s@!¥ =n ! çk ~ =OM !n3 3 r u !E# g %Lz Çè7g`3&Çi!y%,M3 è3 ç è±!yÇW92: Megadható-e valamilyen összefüggés rt és rwu között? 7. Írd le szövegesen az alábbi feladatot: legyen 2m , !ÖEEÝZ é Ù Î s@!Ó Ù Î =n Ù!O Ù M*ë Î![ Î MeÙêlÎ£ ~ =OM ! Ûì tFí Ì|g ahol m#.î½9 , í Ìa! ï ½ ha R '; Ì|! Með>'ñ Ù:Û: Î»ò£ ðF8êlÙ î különben í 8. Igaz-e a specifikáció tételének megfordítása? (Ha megoldja r -et, akkor Nz' s =K{GI J L,{g

5.6. FELADATOK

9. Tekintsük az alábbi feladatot:

55

!E Ô 5 s!¥ Ô =~ Ô(!HÔ MPî> ÚlÔ =OM±5¯Ê.Ì Ù 5·MeÌGÜH½ 5Ê&Ì Ù Ì|ó3 Ôqô^Ì3F¤$3 Ô±ôP5Z3 ahol 5Ê.ÌJÙ G! prímszám . ½&î½. és a zq! õ ö pontokhoz? Mit rendel a fent specifikált feladat az %! Fogalmazd meg szavakban a feladatot!

56

5. SPECIFIKÁCIÓ

Specifikáció A leggyengébb előfeltétel

Recommend Documents