===== 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 =====
  * [[https://is.muni.cz/auth/predmet/fi/IA011|IA011 Sémantiky programovacích jazyků]]

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

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