12. Analýza metod tvorby sémantiky programovacích jazyků

Ako sa učiť?
1) Preletieť tento text: vstrebať, o čom to asi je, dôležité pojmy.
2) Prejsť [Kucera], pochopiť tu spomínané pojmy, pochopiť tam spomínané príklady.
3) Overiť si pochopenie v tomto texte.

Syntax:
1) lexikálne jednotky (kľúčové slová, identifikátory, konštanty, operátory, . . . )
2) frázová štruktúra: určuje aké postupnosti lex. jednotiek sú prípustné.

Sémantika:
1) neformálna: tak ako sme zvyknutý
2) formálna: matematická. IA011.

3 druhy sémantik:
• Operačná sémantika: AKO sa program vykonáva.
• Denotačná sémantika: CO program počíta
• Axiomatická sémantika: umožňuje odvodiť VLASTNOSTI programov.

Nejaké pojmy:
Syntax prog. jazykov: atómy, operácie, konštanty
Syntaktické stromy: induktívna definícia
Odvodzovací systém. Dokázateľnosť tvrdenia.

Indukcie používané v Sémantikách:
• K výške dôkazového stromu
• Štrukturálna

Jazyk IMP
• Základné syntaktické domény
Num = {0, 1, −1, 2, −2, . . .}
Bool = {tt, ff}
Var = {A, B, C, . . .}
• Aritmetické výrazy AEXP
a ::= n | X | a0+a1 | a0−a1 | a0*a1
• Pravdivostné výrazy BEXP
b ::= t | a0=a1 | a0 < = a1 | not b | b0 and b1 | b0 or b1
• Príkazy COM
c ::= skip | X := a | c0;c1 | if b then c0 else c1 | while b do c

Programy majú priradený prechodový systém, ktorý popisuje výpočtové procesy.

STAV: zobrazenie priraďujúce premenným z Var celé čísla.

<a,s> → n …. aritmetický výraz a sa v stave s vyhodnotí na n
<b,s> → t …. pravdivostný výraz b sa v stave s vyhodnotí na t
<c,s> → s' …. príkaz c aktivovaný v stave s skončí v stave s'

Príklad: definícia <a0 + a1, s> → n:

<a0,s> → n0 <a1,s> → n1
————————————- n=n0+n1
<a0 + a1, s> → n

VETA: Pre každé a, b, c, s existuje práve jedno n, t a nanajvýš jedno s', tak že
<a,s> → n … Dôkaz indukciou k štruktúre a
<b,s> → t … Dôkaz indukciou k štruktúre b
<c,s> → s' …Dôkaz indukciou k výške odvodenia

- Pre AExp: a0 ekviv. a1 PODĽA DEFINÍCIE KEĎ forall n in Z, forall stav s : <a0,s> → n ⇔ <a1, s> → n
- Podobne pre BExp a Com.

Prechodová relácia odpovedá 1 kroku výpočtu/1 inštrukcie programu

<a,s> → <a’, s>
<b,s> → <b‘, s>
<c,s> → <c‘,s‘>

Príklad pre + v AExp:

1. pravidlo:

<a0, s> → <a’0, s>
——————————– <a0 + a1, s> → <a’0 + a1, s>

2. pravidlo:

<a1, s> → <a’1, s>
——————————– <n + a1, s> → <n + a’1, s>

3. pravidlo:

<n0 + n1, s> → <m, s>, kde m = n0 + n1

Ako intuitívne chápem rozdiel medzi BIG STEP a SMALL STEP: small step odstraňuje paralelizmus z big stepu. Rodič má v strome vždy len 1 potomok, zatiaľ čo v big step ich mal často niekoľko.

→^* : v konečnom počte prechodov viem doraziť do… (Presná definícia v [Kucera].)

- Aexp: a0 ekviv. a1 PODĽA DEFINÍCIE KEĎ forall n in Z, forall stav s : <a0, s> →^* <n, s> ⇔ <a1, s> →^* <n, s>
- Podobne pre Bexp, Com.

Big Step a Small Step sú ekvivalentné: Presné znenie „ekvivalentnosti“ s nudným technickým dôkazom: [Kucera], Věta 4, str. 144/480.

E: množina všetkých stavov s.

• A : Aexp → (E → Z)
• B : Bexp → (E → T)
• C : Com → (E → E)

Príklady:
A[n]s = n
A[X]s = s(X)
A[a0+a1]s = A[a0]s + A[a1]s
B[a0=a1]s = (A[a0]s = A[a1]s)

Ťažšie definovateľné:
C[if b then c0 else c1]s = C[c0]s ak B[b]s = true
C[if b then c0 else c1]s = C[c1]s ak B[b]s = false

C[while b do c]s … Dlhá teória k CPO, aby sme to vedeli definovať.

Pojmy z CPO:
- CPO: Usporiadaná množina (D, ⇐), kde každý nekonečný reťaz má supremum.
- Monotónna funkcia z jedného CPO do druhého CPO
- Spojitá funkcia: monotónna a supremum obrazov = obraz suprema

Pre nás dôležitá veta:
Nech (D, ⇐) je CPO s najmenším prvkom L a F spojitá funkcia na D. Potom nF = sup_{i in N} F^i(L) je najmenší pevný bod F.

Denotačnú sémantiku while cyklu definujeme postupne cez if-y. Pozri [Kucera], str. 216-236.

<a, s> → n ⇔ A[a]s = n
<b, s> → t ⇔ B[b]s = t
<c, s> → s’ ⇔ C[c]s = s’

{A} c {B} hovorí, že pre každý stav s in E platí: ak s |= A, potom ak c spustený v stave s skončí v stave s’, platí s’ |= B.

{A} c {B} nehovorí nič o tom, čo platí ak c v stave s’ neskončí.

Špeciálny stav L: interpretujeme ako „neskončenie“.

Rozširujeme Aexp do Aexpv:
a ::= n | X | i | a0+a1 | a0−a1 | a0*a1
i in IntVar je množina celočíselných premenných.

Definujeme tvrdenia o programoch… Assn:
A ::= true | false | a0 = a1 | a0 leq a1 | A0 and A1 | A0 or A1 | not A | forall i:A | exists i:A

Interpretácia je funkcia I : IntVar → Z.. Množina všetkých interpretácii sa tiež značí I. Pozn: interpretácia je čosi podobné ako stav, ibaže interpretácia má iné miesto v Assn.

Funkcia E: Aexpv → ( I → (E → Z))
E[n]Is = n
E[X]Is = s(X)
E[i]Is = I(i)
E[a0+a1]Is = E[a0]Is + E[a1]Is

A in Assn je splnené v stave s za interpretácie I keď… [Kucera, 284]

Platné tvrdenie: Značenie: |= {A} c {B} Definícia: [Kucera, 292]

Hoarov odvodzovací systém [Kucera, 300]

Dokázateľné tvrdenie: |- {A} c {B} je dokázateľné tvrdenie, ak je odvoditeľné v Hoarovom odvodzovacom systéme.

Invariant cyklu while b do c je tvrdenie A, pre ktoré platí |= {A and b} c {A}

Veta o korektnosti: |- {A} c {B} implikuje |= {A} c {B}
Veta o úplnosti: |= {A} c {B} implikuje |- {A} c {B}

c0 vlna c1 ⇔ pre každé A, B z Assn: (|={A} c0 {B} ⇔ |={A} c1 {B})

Veta: Pre každé c0, c1 v Com: C[c0]=C[c1] ⇔ c0 vlna c1

Pridáme paralelný operátor ||. Com zmeníme na Pcom, kde je navyše príkaz c0||c1.

Aby to fungovalo ako intuitívne chceme, zavádza sa IsSkip predikát.

Paralelné programy môžu byť NEDETERMINISTICKÉ.

- Verifikácia paralelných a neukončených programov
- LTL a jeho využitie ako jazyka vlastností paralelných a neukončených programov
- w-regulárne jazyky a Buchiho automaty
- Vzťah LTL a Buchiho automatov

• IA011 Sémantiky programovacích jazyků

• http://www.fi.muni.cz/usr/kucera/teaching.html
• [Kucera] http://www.fi.muni.cz/usr/kucera/teaching/semantics/spj.pdf

Michal Abaffy
Moja spokojnosť: 80%. Nespracoval som posledné kapitoly z [Kucera]. Možno budú (sčasti alebo úplne) vypracované v iných otázkach.