Programozás | Programozás-elmélet » Logikák és módszerek a programhelyesség bizonyításához

http://www.doksihu Programozáselmélet Logikák és módszerek a programhelyesség bizonyításához http://www.doksihu Programozáselmélet  Programmodellek       szekvenciális programok rekurzív programok nemdeterminisztikus elemek párhuzamos programok funkcionális programok Programok szemantikája      transzlációs szemantika attribútumnyelvtanok operációs szemantika denotációs szemantika axiomatikus szemantika http://www.doksihu Programozáselmélet Operációs szemantika Szekvenciális programok Rekurzió Nemdeterminisztikus elemek Párhuzamosság Funkcionális programok Denotációs szemantika Axiomatikus szemantika http://www.doksihu Irodalom  Jan van Leeuwen ed.: Handbook of Theoretical Computer Science: Formal Models and Semantics, Elsevier Pub. 1990 – P. Cousot: Methods and Logic for Proving Programs – H. P Barendregt: Functional Programming and Lambda Calculus    H. R Nielson - F Nielson:

Semantics with Applications: A Formal Introduction, 1992. www.daimiaudk/~hrn Kozma L. - Varga L: A szoftvertechnológia elméleti kérdései, ELTE 2003. Csörnyei Z.: Lambda-kalkulus, előadás jegyzet ELTE http://www.doksihu Transzlációs szemantika Program Transzlációs függvény Tárgyprogram Végrehajtás Program output Input adat http://www.doksihu Attribútumnyelvtan Komponensei:  G környezetfüggetlen nyelvtan  A attribútumok rendszere A nyelvtan nemterminális szimbólumaihoz attribútumokat (adott típusú változókat) rendelhetünk, Ezek tartalma lesz a jelentés egyegy komponense. Az attribútumok kétfélék: szintetizáltak és örököltek. Az előbbiek a nemterminálisból levezetett szóból kinyerhető jelentést, míg az utóbbiak a szövegkörnyezet jelentésmódosító hatásait tartalmazzák  P szemantikai egyenletek – Az egyenletekkel lehet definiálni a nyelvtan szabályaiban szereplő nemterminálisok attribútumai közti

összefüggéseket http://www.doksihu Attribútumnyelvtan Egy mondat jelentésének meghatározása: A mondat szintaxisfájában szereplő nemterminálisok attribútumai annyi példányban szerepelnek, ahány példányban maga a nemterminális szerepel. Egy nemterminálisból levezetett részszó jelentését a nemterminális szintetizált attribútumai képviselik, amely függ a külső hatásokat megtestesítő örökölt attribútumuktól. Azaz a kiszámítás folyamatában az örökölt attribútumok az input adatok, a szintetizáltak az outputok. Az attribútumelőfordulások tartalmának meghatározása a szemantikai egyenletek alapján történik. http://www.doksihu Attribútumfüggőségek sémája p A q u B v . Szintetizált attribútumok: q, v, y Örökölt attribútumok: p, u, x x C y http://www.doksihu Példa: Bináris valós konstansok  Környezetfüggetlen nyelvtan:  Attribútumok rendszere: http://www.doksihu Példa: Bináris valós konstansok

 Szemantikai egyenletek és a lokális függőség S v r N v l . r N v l r N v l r N v l r B v http://www.doksihu Példa: Bináris valós konstansok  Szemantikai egyenletek és a lokális függőség r N v l r B v r B v 0 1 http://www.doksihu Szintaxisfa S . N N N B N B 1 0 N N B B 0 1 http://www.doksihu Attribútum előfordulások S v r N v l r N v l r N v l r B v 1 r B v 0 r N v l . r N v l r N v l r B v 0 r B v 1 http://www.doksihu Lokális attribútum függőségek S v r N v l r N v l r N v l r B v 1 r B v 0 r N v l . r N v l r N v l r B v 0 r B v 1 http://www.doksihu Globális attribútum függőségek S v r N v l r N v l r N v l r B v 1 r B v 0 r N v l . r N v l r N v l r B v 0 r B v 1 http://www.doksihu Attribútumok redukálása S v r N v l r N v l r N v l r B v 1 r B v 0 r N v l . r N v l r N v l r B v 0 r B v 1 http://www.doksihu Attribútumok kiértékelése S v

2.25 0 1 r N v 2l r N v 2l r N v l 0 1 r B v 1 0.25 -2 r N v l . 0 r N v l 1 r B v 0 0 2 r N v l 0 -2 r B v r B v 0 1 0 0 2 0.25 http://www.doksihu Operációs szemantika Program Input adat Operációspecifikáció Eredmény Az operációspecifikáció szokásos komponensei:    konfigurációk halmaza operációs reláció: bináris reláció a konfigurációk halmazán (a megtehető elemi operációk halmaza) kezdő konfigurációk, végkonfigurációk http://www.doksihu Denotációs szemantika Program Jelentésfüggvény Matematikai denotáció Az inputot és outputot, és a köztük lévő kapcsolatot kifejező matematikai objektum a matematika nyelvén megfogalmazva http://www.doksihu Axiomatikus szemantika Magasabb absztrakciós szint: nem a program inputja és outputja közti kapcsolat közvetlen leírása a cél.  Feladat (pl. input- és output- feltételpár)  Helyességfogalmak (feladat és program viszonya)  Kalkulus

a helyesség bizonyításához  A helyességet kifejező formulák  Axiómák, levezetési szabályok (pl. Hoare-kalkulus, Dijkstra-kalkulus stb) http://www.doksihu Matematikai jelölések  ∀x∈E. P(x) = ∀x(x∈E ⊃ P(x))  ∃x∈E.P(x) = ∃x(x∈E ∧ P(x))  {F(x) | P(x)} = { y | ∃ x( y =F(x) ∧ P(x))}  〈e1,e2 ,,en 〉∈E n vagy (e1,e2 ,,en )∈E n  r ⊆ E n halmaz komplementere: ¬ r  reláció = részhalmaz  unáris reláció: r ⊆ E   bináris reláció: r ⊆ E 2 két bináris reláció kompoziciós szorzata: r′◊ r″ = {〈e′,e″〉 | ∃e∈E. (〈e′,e〉∈r′ ∧ 〈e,e″〉∈r″ )} diagonális reláció: δ = {〈e,e〉 | e∈E} http://www.doksihu Matematikai jelölések    bináris reláció hatványa: r 0 = δ, r n+1 = r ◊ r n bináris reláció reflexív, tranzitív lezártja: r∗= ∪ { rn | n≥0 } az r bináris reláció bal, ill. jobb oldali leszűkítése a p unáris

relációra: p r = ( p × E ) ∩ r r p = r ∩ ( E × p )  a p unáris relációnak az r bináris reláció szerinti képe: p ◊ r = { e | ∃e′∈p. 〈e′,e〉 ∈ r }  a p unáris relációnak az r bináris reláció szerinti inverzképe: r ◊ p = { e | ∃e′∈p. 〈e,e′〉 ∈ r } http://www.doksihu Matematikai jelölések  kép és inverzkép néhány tulajdonsága ( p, q unáris, r, s bináris relációk):  monotonitás: Ha p ⊆ q és r ⊆ s, akkor p ◊ r ⊆ q ◊ s és r ◊ p ⊆ s ◊ q  asszociativitás: (p ◊ r) ◊ s = p ◊ (r ◊ s) , (r ◊ s) ◊ q = r ◊ (s ◊ q)  hatványhalmaz: P ( E )  fügvényhalmaz: D E  az f ∈ D E függvény értékének a d helyen e -re való módosítása: f de http://www.doksihu Szekvenciális programok - szintaxis     X: Valt E: Kif B: Lkif C: Uts változók kifejezések logikai kifejezések utasítások C = skip | X := E | (C1 ; C2) | (B C1 ◊ C2) | (B ∗

C) Az utasítások neve rendre üres utasítás, (determinisztikus) értékadás, kompozíció, feltételes utasítás, ciklus utasítás. http://www.doksihu Az utasítások szintaxisa B-N-formában 〈utasítás〉 :: = skip | 〈 program változó〉 := 〈kifejezés〉 | 〈utasítás〉 ; 〈utasítás〉 | if 〈logikai kifejezés〉 then 〈utasítás〉 else 〈utasítás〉 fi | while 〈logikai kifejezés〉 do 〈utasítás〉 od http://www.doksihu Operációs szemantika  d:D adatok  s : S = Valt D állapotok  γ : Γ = ( S × Uts) ∪ S konfigurációk http://www.doksihu Kifejezések interpretálása (szemantikája)  I : Kif ( S D)  I : Lkif P ( S ) kifejezések szemantikája jelölés: E = I ( E ) logikai kifejezések szemantikája jelölés: B = I ( B ) http://www.doksihu Példa egy programra és végrehajtására A program: (x:=x-1;(x>0*(y:=y+x;x:=x-1))) Kezdő értékek: x=3 és y=0 x y amit még végre kell hajtani 3

0 2 0 2 0 ((y:=y+x;x:=x-1);(x>0*(y:=y+x;x:=x-1))) 2 2 (x:=x-1;(x>0*(y:=y+x;x:=x-1))) 1 2 1 2 ((y:=y+x;x:=x-1);(x>0*(y:=y+x;x:=x-1))) 1 3 (x:=x-1;(x>0*(y:=y+x;x:=x-1))) 0 3 0 3 (x:=x-1;(x>0*(y:=y+x;x:=x-1))) (x>0*(y:=y+x;x:=x-1)) (x>0*(y:=y+x;x:=x-1)) (x>0*(y:=y+x;x:=x-1)) http://www.doksihu Operációs átmeneti reláció Az operációs átmeneti reláció az utasítások végrehajtása során megtehető lépések halmaza. Op ⊆ Γ × Γ Az utasítások végrehajtásának lépései, azaz az Op reláció elemei pontosan azok a rendezett, konfiguráció párok, amelyek a következőkben felsorolt konstrukciós lépések közül véges sok alkalmazásával előállnak. http://www.doksihu Atomi (egylépéses) utasítások  Az üres utasítás végrehajtása 〈 s , skip〉 Op s minden s ∈ S esetén  Az értékadás végrehajtása 〈 s , X := E 〉 Op s X E ( s ) minden s ∈ S, X ∈ Valt és E ∈ Kif esetén

http://www.doksihu A feltételes utasítás végrehajtásának első lépése  Feltételkiértékelés és belépés a then-ágba 〈 s , (B C1 ◊ C2) 〉 Op 〈 s , C1〉 minden B ∈ Lkif, C1, C2 ∈ Uts és s ∈ B esetén  Feltételkiértékelés és belépés az else-ágba 〈 s , (B C1 ◊ C2) 〉 Op 〈 s , C2〉 minden B ∈ Lkif, C1, C2 ∈ Uts és s ∈¬ B esetén http://www.doksihu A ciklus utasítás végrehajtásának első lépése  Feltételkiértékelés és belépés a ciklusba 〈 s , (B ∗ C) 〉 Op 〈 s , (C ; (B ∗ C))〉 minden B ∈ Lkif, C ∈ Uts és s ∈ B esetén  Feltételkiértékelés és kilépés a ciklusból 〈 s , (B ∗ C) 〉 Op s minden B ∈ Lkif, C ∈ Uts és s ∈¬ B esetén http://www.doksihu A lépések kompozíciós kiterjesztése  Az első komponens végrehajtásának nem utolsó lépése Ha 〈 s′ , C′ 〉 Op 〈 s″ , C″ 〉 és C ∈ Uts, akkor 〈 s′ , (C′ ; C ) 〉 Op 〈 s″ , (C″ ; C

)〉  Az első komponens végrehajtásának utolsó lépése Ha 〈 s′ , C′ 〉 Op s″ és C ∈ Uts, akkor 〈 s′ , (C′ ; C ) 〉 Op 〈 s″ , C 〉 http://www.doksihu Az Op reláció tulajdonságai    S ◊ Op = ∅ Ha C nem kompozíció, akkor | Op( 〈 s , C 〉 ) | = 1 | Op( 〈 s , (C′ ; C ) 〉 ) | = | Op( 〈 s , C′ 〉 ) | http://www.doksihu Az Op reláció tulajdonságai  Ha 〈 s′ , (C′ ; C ) 〉 Op γ, akkor vagy γ = 〈 s″ , (C″ ; C )〉 , vagy γ = 〈 s″ , C 〉  Ha 〈 s′ , (C′ ; C ) 〉 Op 〈 s″ , (C″ ; C )〉, akkor 〈 s′ , C′ 〉 Op 〈 s″ , C″ 〉  Ha 〈 s′ , (C′ ; C ) 〉 Op 〈 s″ , C 〉, akkor 〈 s′ , C′ 〉 Op s″ http://www.doksihu Végrehajtási sorozat A C utasítás s kezdőállapothoz tartozó végrehajtási sorozatának nevezzük konfigurációknak egy véges vagy végtelen { γn } sorozatát, ahol    az első elem γ0 = 〈 s , C 〉, ha Op( γn-1

) ≠ ∅, akkor a sorozatnak van következő, γn eleme, és ekkor γn-1 Op γn http://www.doksihu A végrehajtási sorozat tulajdonságai     Végrehajtási sorozat tetszőleges, legalább kételemű záró szelete szintén végrehajtási sorozat. Determinisztikus utasítás végrehajtási sorozata egyértelmű Ha a determinisztikus utasítás végrehajtási sorozata véges, akkor állapotban végződik Ha az 〈 s , (C1 ; C2 ) 〉 konfigurációval kezdődő végrehajtási sorozat véges, akkor van olyan 〈 s , C1 〉 . s′ végrehajtási sorozat, amelynek C-vel való kompozíciós bővítése kezdőszelete az előbbi sorozatnak. http://www.doksihu A végrehajtási sorozat tulajdonságai  Ha az 〈 s , (B * C)〉 konfigurációval kezdődő végrehajtási sorozat véges, akkor a sorozat, a két szélső eleme nélkül m ≥ 0 db. olyan szakaszra bontható, amely szakaszok valamilyen 〈 s j −1 , C 〉 , . , s j j = 1 . m végrehajtási sorozatok

(B * C) -vel való kompozíciós bővítései