Zadání

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

Vypracování

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.

Úvod

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

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

Operačná sémantika IMP

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

OS prvého typu – BIG STEP

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

Sémantická ekvivalencia výrazov

- 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.

OS druhého typu - SMALL STEP

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.

Sémantická ekvivalencia výrazov

→^* : 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.

Ekvivalencie Big Step a Small Step

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

Denotačná sémantika IMP

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.

Ekvivalencia Operačnej a Denotačnej sémantiky

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

Axiomatická sémantika IMP

{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é a dokázateľné tvrdenia

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}

Ekvivalencia axiomatickej a denotačnej sémantiky

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

Operačná sémantika paralelných programov

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É.

Nespracované

- 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

Předměty

Zdroje

Vypracoval

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

mgr-szz/in-tei/12-tei.txt · Poslední úprava: 2014/10/27 09:07 (upraveno mimo DokuWiki)
Nahoru
CC Attribution-Noncommercial-Share Alike 3.0 Unported
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0