NEM-DETERMINISZTIKUS PROGRAMOK HELYESSÉGE. Szekvenciális programok kategóriái. Hoare-Dijkstra-Gries módszere

2012.10.10.

Szekvenciális programok kategóriái strukturálatlan determinisztikus

NEM-DETERMINISZTIKUS PROGRAMOK HELYESSÉGE

nem-determinisztikus

Hoare-Dijkstra-Gries módszere



Gregorics Tibor

2.

 1.

o

3

Floyd módszerének felidézése

Gregorics Tibor

Szintézis és verifikáció

4

A nem-determinisztikusság miatt egy rögzített kezdő csomóponthoz és kiinduló állapothoz többféle végrehajtás is tartozhat.  Egy végrehajtáshoz ugyan most is egyértelműen tartozik egy út a program-gráfban, de adott kiinduló állapot mellett egy úton több végrehajtás is keletkezhet.  A Floyd módszer tehát nem-determinisztikus program esetén is alkalmazható, de az útszakasz jellemzők felírása körülményesebb. Erre megoldást jelenthet, ha sűrűn címkézzük a program-gráfot (minden csomópont előtt és után), de ekkor a helyességbizonyítás a sok útszakasz miatt hosszadalmas.

egy rögzített kezdő csomóponthoz és kiinduló állapothoz egyértelműen tartozott egy végrehajtás és egy út a program-gráfban.  Floyd módszere úgy mutatta meg, hogy bármelyik 𝜑 -ből induló végrehajtás 𝜓-ben áll meg, hogy a program-gráfnak a végrehajtáshoz tartozó útját, pontosabban annak útszakaszait vizsgálta.  Ennek alapja az volt, hogy adott kiinduló állapot mellett egy út egyértelműen azonosította a végrehajtást. Szintézis és verifikáció

A gyűjtő csomópontokba kettőnél több él is befuthat.

Floyd módszer általánosítása

 Determinisztikus programok esetében

Gregorics Tibor

2

Ha egyszerre több kivezető él feltétele is teljesül, akkor az egyik ilyen ág hajtódik végre. Ha egyik feltétel sem teljesül, ekkor hibás működés keletkezik.

◦

Ez átvezet a párhuzamos programok vizsgálatához, ezért itt nem is számolunk vele



v ← f(v) helyett: v ← e ha e∊ f(v) (v :∊f(v) ) Ennek alesete a v ← f(v) g(v) f, g : A → A, amikor v ← f(v) vagy v ← g(v) hajtódik végre.

◦

3. Gregorics Tibor

fejlett

Az elágazási csomópontoknál megengedünk kettőnél több kivezető élt is, amelyekhez egy-egy kvantorfüggetlen logikai kifejezés tartozik.

2.

Nem-determinisztikus szekvencia, azaz nincs megkötés a szekvenciát alkotó tagprogramok sorrendjére

3.

általános

A programok leírására a determinisztikus programoknál bevezetett gráfot használhatjuk: A számítási csomópontokban megengedjük, hogy az f számítás nem-determinisztikus legyen: f  A × A. ◦ ◦

Az átfedő feltételek okozzák a nem-determinisztikusságot Ha egyik feltétel sem teljesül, ekkor hibás lesz a működés

o o

korai

Program-gráf

A számítási csomópontokhoz nem függvényt, hanem relációt (nem-determinisztikus függvényt) rendelünk. Az elágazási csomópontoknál kettőnél több kivezető él lehet, és mindegyikhez tartozik egy feltétel, ám ezek a feltételek nem szükségképpen teljesek és diszjunktak páronként.

1.

valódi

Először általában a nem-determinisztikus programok formális helyesség bizonyításait vizsgáljuk Majd a nem-determinisztikus strukturált programok szintéziséről lesz szó



Nem-determinisztikus program elemek

strukturált



5

Gregorics Tibor


6

1

2012.10.10.

Nem-determinisztikus strukturált programok  A strukturált programokat most

Szintaxis 1. őrfeltételes (parciális) értékadás

is rekurzív módon

definiáljuk. definíciót is fogunk látni

kiválasztás

 Kétféle

iteráció

S::= skip   v f(v) S1; S2 if 1 S1  …  n  Sn do 1 S1  …  n  Sn do

kilépéses iteráció

Gregorics Tibor


7

Szemantika 1.     




9

◦ S1, S2 … ,Sn, Se nem-determinisztikus programok ◦ f : A→ A; f(v) kifejezés ◦ 1 , … , n,  : A→ 𝕃; i(v),  (v) kvantorfüggetlen logikai kifejezések

Gregorics Tibor


8

S::= skip v: f(v) S1; S2 if 1 S1  …  n  Sn fi while (v) do S0 od

   

ahol

◦ S0, S1, S2 … ,Sn nem-determinisztikus programok ◦ f  A×A ◦ 1 , … , n : A→ 𝕃; i(v) kvantorfüggetlen logikai kifejezések

Gregorics Tibor


10

Leggyengébb előfeltétel (Dijkstra)

Szemantika 2. 

1 S1  …  n  Sn  Se; exit od

ahol

Szintaxis 2.

skip () =     () (   v  f(v))( )=   , f()  () (   v  f(v))( )=   , fail  fail,  M[S1]() (S1; S2 )() = S1()  S2(M[S1]() ) fail,  M[S1]() (S1; S2 )() = S1() i[1..n]:  i() (if 1 S1  …  n  Sn fi)( ) = S i ( ) i[1..n]: i() (if 1 S1  …  n  Sn fi)( ) =   , fail i[1..n]: i() (do 1 S1  …  n  Sn od)() = (S i; do  1 S1  …  n  Sn od)() i[1..n]: i() (do 1S1  …  nSn od)( ) =  i[1..n]: i() (do 1S1  …  nSn  Se ; exit od)() = (S i; do  1S1  …  nSn  Se ; exit od)() i[1..n]: i() (do 1S1  …  nSn Se ; exit od)()=Se ()

Gregorics Tibor

fi od

    

 Legyenek ahol

skip () =   

Q, R : A → 𝕃 állítások és S egy

program 

(v : f(v))( )=  (v) , e, ahol e  f()



fail,  M[S1]() (S1; S2 )() = S1()  S2(M[S1]() ) fail,  M[S1]() (S1; S2 )() = S1()



i [1..n]:  i() (if 1 S1  …  n  Sn fi)( ) = S i( ) i[1..n]: i()  (if 1 S1  …  n  Sn fi)( ) =   , fail



()  (while (v) do S1 od )() = (S1; while (v) do S1 od )() ()  (while (v) do S1 od )() = 

leggyengébb előfeltétele [lf(S ,R)] = { 𝜎∊ Dp(S)  p(S)(𝜎)  [R] }

 Dijkstra

Gregorics Tibor


 {Q}

S {R} helyett használjuk: Q ⇒ lf(S ,R)

 Teljes

11

helyesség feltétele: ◦  ⇒ lf(S , ) ahol (, ) a feladat specifikációja ◦ bB-re: Qb ⇒ lf(S , Rb)

Gregorics Tibor


12

2

2012.10.10.

Hoare-Dijkstra-Gries módszer axiómái és szabályai nem-determinisztikus programokra

Hoare axiómái és szabályai a leggyengébb előfeltétel használatával  

Üres program: Értékadás:

lf(skip, R) = R lf(v f(v), R) =R∘f

 

f totális 

 

Szekvencia: Q ⇒ lf((S1;S2), R) ha Q ⇒ lf(S1, Q’) és Q’ ⇒ lf(S2, R) ahol Q’ : A → 𝕃 Elágazás: Q ⇒ lf(if  then S1 else S2 fi, R) ha Q   ⇒ lf(S1, R) és Q   ⇒ lf(S2, R) Ciklus: Q ⇒ lf(while  do S0 od) , R) ha Q ⇒ P és P   ⇒ R és P   ⇒ lf(S0,P) és P   ⇒ t>0 és t0∊ℤ: P   t=t0 ⇒ lf(S0, t
Gregorics Tibor


13

Üres program: lf(skip, R) = R Értékadás: lf(v:∊f(v), R)(v) = v∊Df  ∀e∊ f(v) : R(e)



Szekvencia: Q ⇒ lf((S1;S2), R) ha ∃Q’ : A → 𝕃 úgy, hogy Q ⇒ lf(S1, Q’) és Q’ ⇒ lf(S2, R)



Elágazás: Q ⇒ lf(if 1 S1  …  n  Sn fi, R) ha Q ⇒ 1 …  n és ∀i ∊{1 .. n}: Q  i ⇒ lf(Si, R)



Ciklus: Q ⇒ lf(while  do S0 od) , R) ha ∃ I : A → 𝕃 és ∃ t : A → ℤ úgy, hogy Q ⇒ I és I   ⇒ R és I   ⇒ lf(S0, I) és I   ⇒ t>0 és t0∊ℤ: I   t=t0 ⇒ lf(S0, t
Gregorics Tibor


14

h := 1

Példa

Példa folytatása 

Valós szám természetes számú hatványa A = ℝℕℝ x n h Q = (x=x’  n=n’) R = (h = x’n’ )

 

I = (h*xn = x’n’ ) t=n



h := 1 n0 h, n := h * x, n – 1

Gregorics Tibor


15

Példa befejezése

Gregorics Tibor

 

2.

b) c) d)

I⇒I I  n=0 ⇒ R


16

Példa

I = h*xn = x’n’ 1. Q ⇒ Ih←1=(h* xn = x’n’ ) h←1= (xn = x’n’ )

a)

n0

Kell: Q ⇒ lf(S, R) h, n := h * x, n – 1 Elég: 1. Q ⇒ lf(h := 1, I) Elég: Q ⇒ Ih←1 2. I ⇒ lf(while, R) Elég: a) I ⇒ I b) I  n=0 ⇒ R c) I  n≠0 ⇒ t>0 d) I  n≠0  t=t0 ⇒ lf(h, n := h * x, n – 1, I  t0

~ h* xn = x’n’  n=0 ⇒ h = x’n’

I  n≠0 ⇒ n>0~ h* xn = x’n’  n≠0 ⇒ n>0 (n : ℕ) I  n≠0  n=n0 ⇒((I  n0 )= =( h*x* xn-1 = x’n’  n-10 ) (n : ℕ)



Két természetes szám legkisebb közös többszöröse A = ℕℕℕ a b c Q = (a=a’  b=b’  a>0  b>0) R = (Q  d = lkkt(a,b) ) I = (Q  ad  bc  max(d,c) lkkt(a,b) ) t = lkkt(a,b)–max(d,c) d, c := a, b dc

I

Gregorics Tibor


17

Gregorics Tibor

d
d>c

d := d+a

c := c +b


18

3

2012.10.10.

d, c := a, b

Példa folytatása 

Kell: Q ⇒ lf(S, R) Elég: 1. Q ⇒ lf(d,c := a,b, I) Elég: Q ⇒ Id,c←a,b 2. I ⇒ lf(while, R) Elég: a) I ⇒ I b) I  d=c ⇒ R

d
d>c

d := d+a

c := c +b

c)

I  d≠c ⇒ t>0

d)

I  d≠c  t=t0 ⇒ lf(if, I  t
Gregorics Tibor

Példa folytatása

dc


I  d≠c  t=t0 ⇒ lf(if, I  tc ii. I  d≠c  t=t0  dc ⇒ lf(c := c +b, I  tc ⇒ (I  t
d)

19

Példa befejezése

Gregorics Tibor

lf(skip , R)=R helyett [lf(skip , R)]=[R]

2.

I⇒I b) I  d=c ⇒ R (ad  bd  d lkkt(a,b) ⇒ d= lkkt(a,b)) c) I  d≠c ⇒ lkkt(a,b)–max(d,c)>0 (lkkt(a,b)≠max(d,c)) i. I  d≠c  lkkt(a,b)–max(d,c)= t0 ⇒ dc ii. I  d≠c  lkkt(a,b)–max(d,c)=t0  dc ⇒ Q  ad  b(c+b)  max(d,c+b) lkkt(a,b  lkkt(a,b)–max(d,c+b)


[lf(skip , R)] = { 𝜎∊ Dp(skip)  p(skip)(𝜎)  [R] } = = { 𝜎∊A 𝜎∊[R] } = [R]



[lf( v:∊f(v) , R)] = { 𝜎∊ Dp(v:∊f(v))p(v:∊f(v))(𝜎)[R]} = = { 𝜎∊ Df f(𝜎)[R]} = ( { 𝜎∊ Df  ∀e∊ f(𝜎) : R(e)} ) = = { 𝜎∊ Df 𝜎[R∘f]} = Df [R∘f]

a)


21

Szekvencia levezetési szabályának helyessége

lf( v:∊f(v) , R)= v∊Df  ∀e∊f(v) : R(e) helyett [lf(v:∊f(v) , R)]=Df [R∘f]

Gregorics Tibor

Elég belátni: ◦ [Q]  [lf(S1, Q’)]  [lf(S1, lf(S2, R))] = [lf((S1;S2), R)] Monotonítási szabály





Szekvencia definíciója

Kevésbé formálisan: ◦ Az (S1;S2) szekvencia összes végrehajtása (ld. szekvencia definíciója) az S1-beli végrehajtással indul. Egy Q-ból induló végrehajtásnak az első szakasza ezért a Q ⇒ lf(S1, Q’) miatt véges lépésben eljut Q’-be, ahonnan az S2 folytatja a végrehajtást (ld. szekvencia definíciója). Ez a második szakasz a Q’ ⇒ lf(S2, R) miatt R-ben fog megállni, tehát a szekvencia Q-ból induló végrehajtása R-ben áll meg, azaz Q⇒lf((S1;S2), R).

Gregorics Tibor



22

Elágazás levezetési szabályának helyessége

Q ⇒ lf(S , R) helyett [Q]  [lf(S , R)]



20

Axiómák helyessége

I = Q  ad  bc  max(d,c) lkkt(a,b) 1. Q ⇒ Id,c←a,b =(Q  ad  bc  max(d,c) lkkt(a,b))d,c←a,b =(Q  aa  bb  max(a,b) lkkt(a,b) )

Gregorics Tibor


23

Bizonyítás: ◦ Vegyünk egy Q-beli q állapotot. A q az elágazás valamelyik feltételét biztosan kielégíti a Q ⇒ 1 …  n miatt, ezért az elágazás definíciója szerint belőle csak olyan végrehajtások indulnak, amelyeket azok az ágak adják, amelyek feltételét a q állapot kielégíti. ◦ Mivel ∀i ∊{1 .. n}: Q  i ⇒ lf(Si, R) ezért mindegyik q-ból induló végrehajtás R-ben áll meg, azaz Q ⇒ lf(if 1 S1  …  n  Sn fi, R) .

Gregorics Tibor


24

4

2012.10.10.

Ciklus levezetési szabályának helyessége 

Ciklus levezetési szabályának helyessége

Bizonyítás: ◦ Egy ciklus minden végrehajtása felbontható a ciklusmag végrehajtásaiból áll szakaszokra (kivéve a -beli állapotból induló végrehajtásokat).  ezek a szakaszok mindig egy -beli állapotból indulnak (hiszen S0 csak ekkor kap szerepet)  az I-ből induló szakaszok az I⇒lf(S0, I) miatt I-ben állnak meg (eredményesen). ◦ A ciklus eredményesen megálló végrehajtásai -beli állapotban végződnek  vagy -beli állapotból induló egyelemű végrehajtás  vagy a végrehajtás legutolsó szakasza -beli állapot kell legyen

Gregorics Tibor




25

Bizonyítás folytatása: ◦ A Q-ból induló és eredményesen (-ban) leálló végrehajtások a Q⇒I miatt I-ből indulnak, így aztán minden szakasz határa I-ben lesz, tehát a végrehajtás végállapota is, ami az I⇒R miatt R-ben lesz. ◦ A Q-ból induló végrehajtások mind eredményesek, mert az I-ből induló szakaszai mind eredményesek, és végtelen sok szakasz nem lehet. Ez utóbbi esetén ugyanis I⇒t>0 és t0∊ℤ: I   t=t0 ⇒ lf(S0, t
Gregorics Tibor


26

A módszer helyes, de nem teljes előbbi bizonyítások alapján ⇒ a módszer helyes állításoknak egy kivételével a megfordítása is igaz.

 Az

 A bizonyított o

o

A ciklus levezetési szabályának megfordítása viszont csak akkor igaz, ha a ciklusmag iterációinak száma a feladat kezdőállapotaiban felülről becsülhető. Van olyan nem-determinisztikus ciklus (program), amely megold egy problémát, de a ciklus levezetési szabályának (leállási) feltételei nem teljesülnek rá. A=ℤ n Q = (igaz) R = (n=0)

Gregorics Tibor


n0 n<0 n :∊ ℕ

n := n ‒ 1 27

5

NEM-DETERMINISZTIKUS PROGRAMOK HELYESSÉGE. Szekvenciális programok kategóriái. Hoare-Dijkstra-Gries módszere

Recommend Documents