Kiterjesztések szemantikája • Példa • DInteger = { ..., -1,0,1, ... }; DBoolean = { true, true, false } … • DT1 × ... × Tn → T = DT1 × ... × DTn → DT Az összes fü függvé ggvény halmaza, amelyek a DT1 ,..., DTn halmazokbó halmazokból DT halmazra ké képeznek le. • l(c) értelmezé rtelmezés • Az alaptí alaptípusok minden konstansa sajá saját magá magának az értelmezett érté rtéke: ha c alaptí alaptípusú pusú, akkor l(c) = c • Példa • Az 1 Integer konstans értelmezi az 1 Integer számot. • A true Boolean konstans értelmezi a true Boolean értéket.
Determinisztikus program • A determinisztikus program egy szimbólumokból képzett string • Kulcsszavak: if, then, else, fi, while, do, od • A programot generáló grammatika • S ::= skip | u := t | S1; S2 | if B then S1 else S2 fi | while B do S od (Az S, S1, S2 programok változói egyszerű, vagy indexes változók) • Példa • u egy egyszerű vagy indexes változó, t egy kifejezés és • u és t típusa megegyezik, • B egy kvantor-független logikai kifejezés if B then S fi ≡ if B then S else skip fi
Determinisztikus program jelentése • Az S determinisztikus program jelentése • A megfelelő (kezdő) állapotok halmazáról megfelelő (vég-)állapotok halmazára történő leképezés: Divergencia végállapotának jele:
M[S]
⊥
• Denotációs szemantika-definíciós módszer • Operációs szemantika-definíciós módszer (minden programtípusra kézenfekvő)
• Adott absztrakt gép, S program megfelelő Σ állapothalmaz esetén az absztrakt gép konfigurációja: < S, σ >, ahol σ ∈ Σ • A program végrehajtása konfigurációk közötti átmenetek sorozata.
Kofiguráció-átmenet, befejeződés • Konfigurációk közötti átmeneti reláció (transition relation): → • Konfigurációk közötti átmenet • konf1 → konf2 • <S, σ> →
• σ, τ ∈Σ, R: maradék program • Befejeződés • A program végrehajtásának befejeződésének eredménye
R ≡ E : üres program
• ekkor a program befejeződik a τ állapotban.
Nyelvi szerkezetek szemantikája • Axiómák • Üres utasítás: • Értékadás:
< skip, σ > → < E, σ > < u := t, σ > → < E, σ(u := σ(t)) >
• Következtetési szabályok • Szekvencia: S1 ; S2
<S1, σ> → <S2, τ> <S1;S, σ> → <S2;S, τ>
• Feltételes elágazás: if α then S1 else S2 fi < if α then S1 else S2 fi,σ > → <S1, σ> ha σ(α) = T; < if α then S1 else S2 fi,σ > → <S2, σ> ha σ(α) = F;
Nyelvi szerkezetek szemantikája • Következtetési szabályok (folytatás) • Iteráció: while B do S od < while B do S od, σ > → < S; while B do S od, σ> < while B do S od, σ > → < E, σ>
• Megszakítás nélkül végrehajtódnak • skip, • értékadás, • bool kifejezés kiértékelése.
ha σ(B) = T, ha σ(B) = F.
Determinisztikus programok • S program σ állapottal kezdődő tranzakciós sorozata • Konfigurációk véges, vagy végtelen sorozata: <Si, σi> • <S, σ> = <S0, σ0> → <S1, σ1> → . . . → <Si, σi> → ...
(i ≥ 0)
• Az S program σ állapottal kezdődő kiszámítása egy olyan tranzakciós sorozat, amely nem bővíthető. • Az S program σ állapottal kezdődő kiszámítása τ állapotban befejeződik, ha a sorozat véges és annak utolsó konfigurációja: <E, τ> ahol E az üres (empty) program. • Az S program σ kezdő állapottal kezdődő kiszámítása divergens, ha a sorozat végtelen.
Determinisztikus programok • S program kiszámítása egy adott σ kezdő állapottal • η: < S, σ > → < S1, σ1 > → ... → < Sn-1, σn-1 > → < Sn, σn > • Ha a program végrehajtása véges és eredményesen befejeződik • η: < S, σ > → < S1, σ1 > → ... → < Sn-1, σn-1 > → < Sn, σn > • val(η η) = σn, σn ∈ Σ =T (üres program) • Sn • Rövid jelölés: η: < S, σ > → * < Sn, σn > • Ha a program végrehajtása véges, akkor Sn üres program (E). Mivel E = T (vagyis terminál), így ha a program végrehajtása hibás, akkor • η: < S, σ > →* < E, fail > • val(η) = fail, fail ∈ Σ • Sn = E, (üres program) •E = T.
Determinisztikus programok • Lemma
• Indoklás
Minden S determinisztikus programhoz adott σ megfelelő állapot mellett pontosan egy kiszámítás tartozik. Minden konfigurációnak pontosan egy rákövetkezője van a sorozatban.
• Definíció
Blokkolás mentesség Ha S ≠ E és minden σ∈Σ esetén létezik olyan <S1,τ> konfiguráció, melyre <S, σ> → <S1, τ>, akkor a programot blokkolás mentesnek nevezzük.
• Lemma • Indoklás
Minden determinisztikus program blokkolás mentes. Ha S ≠ E, akkor minden <S, τ> konfigurációra létezik egy rákövetkező konfiguráció a → reláció szerint.
Determinisztikus program szemantikája
• Parciális helyességi szemantika • M[S] : Σ → P(Σ) • M[S](σ) = { τ | < S, σ > →* < E, τ > } • Teljes helyességi szemantika • Mtot[S] : Σ → P( Σ ∪ { ⊥ } ) • Mtot[S](σ) = M[S](σ) ∪ { ⊥ | S divergálhat σ kezdeti értékkel }
Példa S ≡ a[0]:=1; a[1]:=0; while a[x]≠0 do x:= x+1 od; Legyen σ∈Σ, amelyben x=0; Determinizmus alapján egy kiszámítás létezik <S,σ> kezdőérték esetén {σ∈Σ ∧ x=0} < a[0]:=1; a[1]:=0; while a[x]≠0 do x := x+1 od, σ >; → {x=0 ∧ a[0]=1} < a[1]:=0; while a[x]≠0 do x := x+1 od, σ[a[0]:=1] > → < while a[x]≠0 do x := x+1 od, σ' > → (σ': σ[a[0]:=1][a[1]:=0]; ami a σ ismételt aktualizálását jelenti),
< x:= x+1; while a[x]≠0 do x := x+1 od, σ' > → < while a[x]≠0 do x := x+1 od, σ'[x:=1] > → <E, σ'[x:= 1] >. M[S](σ) = Mtot[S](σ) = { σ'[x:= 1] }
Példa Legyen τ ∈ Σ olyan állapot, amelynél x = 2 és i = 2, 3, ... , a[ i ] = 1; S ≡ a[0]:=1; a[1]:=0; while a[x] ≠ 0 do x := x+1 od; Induláskor <S, τ> → < a[1]:=0; while a[x] ≠ 0 do x := x+1 od, τ[a[0]:=1] > → while a[x] ≠ 0 do x := x+1 od, τ' > → < (τ': τ[a[0]:=1][a[1]:=0]; ami a τ ismételt aktualizálását jelenti). < x := x+1; while a[x] ≠ 0 do x := x+1 od, τ' > → < while a[x] ≠ 0 do x := x+1 od, τ'[x := τ(x)+1] > →* < while a[x] ≠ 0 do x := x+1 od, τ'[x := τ(x)+k] > → … • S végrehajtása divergens • M[S](τ) = ∅ • Mtot[S](τ) = { ⊥ }
A szemantika tulajdonságai • Ha Ω egy üres determinisztikus program, akkor • ∀σ∈Σ : M[Ω Ω](σ σ) = ∅ • Példa while true do skip od • Az iteráció induktív definíciója: • (while B do S od)0 = Ω, • (while B do S od)k+1 = if B then S; (while B do S od)k else skip fi; • M[S]( ⊥ ) = ∅, Mtot[S](⊥) = { ⊥ } • N[S]:
M[S], Mtot[S]
• N[S](X) = ∪ N[S](σ) σ∈X
és X ⊆ Σ ∪ { ⊥ } esetén
A szemantika tulajdonságai • N[S] monoton • Egy adott program utasításainak halmazát tekintve ha X ⊆ Y ⊆ Σ ∪ {⊥}, akkor N[S](X) ⊆ N[S](Y) • Kompozíció tulajdonság • N[S1; S2](X) = N[S2](N[S1](X)) • Asszociatív a program utasításaira nézve • N[(S1; S2); S3](X) = N[(S1; (S2; S3)](X) • Feltételes elágazás tulajdonsága • N[if B then S1 else S2 fi)](X) = N[S1](X ∩ {B}) ∪ N[S2](X ∩ {~B}) ∪ {⊥⊥∈ X and N = Mtot) • Iteráció tulajdonsága k=∞
• M[while B do S od] = ∪ M[(while B do S od)k] k=0
A szemantika tulajdonságai • Az iterációs tulajdonság Mtot szemantikára nem igaz k=∞
M[while B do S od] = ∪ M[(while B do S od)k] k=0
• Bizonyítás • Tegyük fel hogy igaz. • Mivel minden σ∈Σ esetén Mtot[Ω](σ) = {⊥}, ezért k=∞
⊥∈ ∪ Mtot [(while B do S od)k](σ) k=0
minden • De létezik olyan
while B do S od
program esetén.
while B do S od,
amelyre
⊥ ∉ Mtot [while B do S od](σ) • Ellentmondás!
Bool feltétel, állapot transzformáció • Definíció (bool feltétel, állapot transzformáció) • Adott Σ állapot halmaz, és σ ∈ Σ állapot mellett a Bool feltétel egy bool függvény, amely a szóban forgó állapothoz az igaz értéket rendeli: Σ → bool • Az f állapot transzformáció a Σ → Σ leképezések egy eleme. • Szemantika hozzárendelése a változókhoz • Adott a program változóinak egy x = (x1, ..., xn) sorozata és a megfelelő d = (d1, ..., dn) értékek egy sorozata. • A megfeleltetés di
ha y = xi,
• (σ: x→d)(y) = σ(y) ha y ≠ xi
i = 1, ..., n
• Szemantikailag az állapot hozzárendelése a változókhoz:
σ: x → d
Szekvenciális tranzakciós diagram • Szekvenciális tranzakciós diagram • a program vezérlési szerkezetét írja le. • Szerkezete • A program végrehajtási pontjait és a pontok közötti átmeneteket (transitions) tartalmazza. • Végrehajtási hely • a program számlálónak (counter) a helyzetét mutatja. • Átmenet • a tranzakció az utasítás végrehajtásának a hatását adja meg a programszámláló új értékének a formájában. • Egy utasítás végrehajtása • állapot transzformáció formájában valósul meg • az állapot a memória tartalmát fejezi ki, • az állapot transzformációk a memória cellákhoz a végrehajtott operációk eredményeit rendelik.
Szekvenciális tranzakciós diagram • A program vezérlési szerkezete egy címkékkel ellátott irányított gráf. • Tranzakciós diagram T = ( L, T, s, t ) • Gráf csúcsok
a program állapotai
• entry kitüntetett csúcs: indulási állapotot azonosító cimke: s • exit kitüntetett csúcs: befejező állapotot azonosító cimke: t •L
állapotokat azonosító címkék halmaza: l ∈ L
l
• A gráfban minden él egy állapotátmenet, melyhez egy utasítás c→f
tartozik címkeként: l •c •f
logikai feltétel, állapot transzformáció.
• (l, c → f, l') ∈T
állapotátmenetek halmaza.
l'
Tranzakciós diagram kiszámítása • Egy P = (L, T, s, t) tranzakciós diagram egy η végrehajtása (kiszámítása) a σ0 kezdőértékkel a kezdő l0 címkétől 〈 li, σi 〉 konfigurációk egy sorozata: ahol l0 = s.
η: 〈 l0, σ0 〉 → 〈 l1, σ1 〉 → 〈 l2, σ2 〉 → ...
• Minden tranzakcióhoz létezik
l
c→f
l'
úgy, hogy c(σi) = true és σi+1 = f(σi) • A sorozat nem bővíthető • Ha véges, akkor az utolsó konfigurációnak nincs rákövetkezője.
Tranzakciós diagram kiszámítása • Ha a sorozat véges és az utolsó konfiguráció: 〈 t, τ 〉 • val(η) = τ
(τ ∈ Σ)
• Ha a sorozat véges és az utolsó konfiguráció: 〈 ln, τ 〉, ln ≠ t • val(η η) = fail • Ha a sorozat végtelen • val(η) = ⊥
(⊥, fail ∉Σ)
• comp(P)(σ): P kiszámításainak halmaza, a σ kiindulási állapot mellett. • A P tranzakciós diagram jelentése: M[P](σ) = { val(η) | η ∈ comp[P](σ) }
