Denotacijska Semantika

Denotacijska semantika je način opisa programskega jezika, s katerim damo jeziku natančen pomen. Če je sintaksa jezika skoraj vedno opisana z varianto BNF notacije, pa je semantika oz. pomen jezika prepuščen opisu z naravnim jezikom, kar je lahko zelo dvoumno.

V denotacijski semantiki definiramo jezik s semantično funkcijo, ki program preslika v skupek matematičnih objektov, upoštevajoč njihovo denotacijo (pomen). Tako je razmišljanje o pomenu programov lahko zoženo na razmišljanje o pomenu njihovih denotacij. Če imata dva programa enako denotacijo, potem bosta vrnila enak rezultat.

Definicija pomena jezika

Definicija sintaktične domene

Sintaktično domeno opišemo z BNF notacijo.

Definicija semantične domene in stanja

Stanje lahko opisuje nek kos pomnilnika, ki predstavlja trenutno stanje programa. Največkrat je definirano kot kartezični produkt vseh spremenljivk v programu (kartezični produkt ustreznih množic, katerih elemente lahko zavzamejo posamezne spremenljivke).

Primer definicije stanja:

za opis semantike programa, v katerem lahko naslavljamo samo tri spremenljivke v obsegu naravnih števil (v računalništvu sicer ne moremo obravnavati poljubno velikega naravnega števila, vendar to za semantično obravnavo ni pomembno), lahko stanje definiramo kot:

Definicija semantičnega pomena programa se navezuje na sintaktično domeno. Denotacijsko semantiko definiramo kot množico semantičnih funkcij, ki ustrezajo posameznim pravilom BNF sintakse. Posamezna funkcija preslika določeno sintaktično drevo (strukturo v katero razvijemo sintaktično pravilen program, ali del programa) v določen matematični objekt. Matematični objekt je element določene množice - ponavadi je to funkcija (matematična ali podana s psevdokodo) ali neko število.

Primer definicije domene semantične funkcije:

Poglejmo primer iz prvega zgleda. Definirali bomo semantično domeno za funkcijo M_exp, ki slika sintaktično drevo ki ga generira sintaktično pravilo <exp> v rezultat izraza.

Domeno funkcije definiramo kot

Razlaga zgoraj navedene definicije: funkcija M_exp slika sintaktično drevo Exp v funkcijo f: State → {true, false} - torej v funkcijo ki slika stanje (torej vrednosti spremenljivk) v končni rezultat, ki je eden izmed objektov iz množice {true, false}.

Definicija semantične funkcije

V tem koraku dokončno definiramo semantične funkcije. Definirali smo že semantično domeno, vendar je treba določiti še dejanske preslikave. Za boljše razumevanje si poglejmo primer definicije:

Primer iz prvega zgleda - definicija semantične funkcije M_exp:

Mexp [e: exp] (s: State) ≡
      <fact> and <exp> ⇒ Mfact[e.fact](s) AND Mexp[e.exp](s) |
      <fact> or <exp> ⇒ Mfact[e.fact](s) OR Mexp[e.exp](s) |
      <fact> ⇒ Mfact[e.fact](s)

Razlaga: oglati oklepaji obsegajo parametre podane semantični funkciji, torej ustrezno sintaktično drevo. Za znakom '≡' sledi definicija. Ker se lahko vsako sintaktično drevo že v korenu razdeli na več načinov, se tudi pri definiciji semantične funkcije podobno kot pri BNF notaciji uporablja simbol '|' za ločevanje možnosti. Vsaka možnost vsebuje definicijo funkcije za posamezno sintaktično razvejitev - preslikavo v ustrezen matematični objekt. Če je objekt funkcija se v začetku definicije (pred '≡') dodajo še navadni oklepaji znotraj katerih so zajeti parametri, ki se podajo funkciji, ki jo kot rezultat vrne semantična funkcija (M_exp [e: exp] vrne funkcijo in ne števila). Če v konkretnem primeru pogledamo prvo možnost preslikave: če je e definiran kot <fact> and <exp> potem semantična funkcija za to drevo vrne funkcijo, ki ustreza logičnemu in vrednosti funkcij, ki ju dobimo iz poddreves s pomočjo ustreznih semantičnih funkcij. Funkcijama podamo kot parameter nespremenjeno stanje s.

Primeri

Boolovi izrazi

Primer 1

Naloga: Definiraj sintakso in semantiko preprostih boolovih izrazov. V izrazih lahko nastopajo spremenljivke x, y in z, ki imajo nedefinirano vrednost (true ali false), konstanti true in false ter operatorji and, or in not.

Nekaj primerov sintaktično pravilnih izrazov:

a) z
b) x or ( y and not z )
c) not x and ( true and ( false or y ) )

Rešitev:

1. Sintaktična domena (v BNF notaciji)

<exp> ::= <fact> "and" <exp> | <fact> "or" <exp> | <fact>
<fact> ::= "true" | "false" | "not" <fact> | <var1> | ( <exp> )
<var1> ::= "x" | "y" | "z"

2. Opis stanja in semantičnih funkcij

Stanje opisujejo vrednosti spremenljivk x, y in z:

State ≡ {true, false} × {true, false} × {true, false}

<exp>, <fact> ter <var1> preslikajo trenutno stanje spremenljivk x, y, in z v vrednost izraza (oz. dejstva ali spremenljivke) true ali false:

Mexp: exp → (State → {true, false})
Mfact: fact → (State → {true, false}) 
Mvar1: var1 → (State → {true, false})

3. Definicija semantičnih funkcij

Mexp[e: exp](s: State) ≡
  <fact> and <exp> ⇒ Mfact[e.fact](s) AND Mexp[e.exp](s) |
  <fact> or <exp> ⇒ Mfact[e.fact](s) OR Mexp[e.exp](s) |
  <fact> ⇒ Mfact[e.fact](s)

Mfact[f: fact](s: State) ≡
  true ⇒ true |
  false ⇒ false |
  <var1> ⇒ Mvar[f.var1](s) |
  not <fact> ⇒ NOT Mfact[f.fact](s) |
  <exp> ⇒ Mexp[f.exp](s)

Mvar1[v: var1](<xVal, yVal, zVal>: State) ≡
  x ⇒ xVal |
  y ⇒ yVal |
  z ⇒ zVal

Primer 2

Naloga: Denimo da je vrednost stanja State = <true, true, true>, in je pomen Boolovega izraza definiran kot v rešitvi zgleda 1. Kakšen je potem pomen izraza:

x or ( y and not z )?

Torej:

Mexp[x or ( y and not z )](<true, true, true>) = ?

Rešitev:

Mexp[x or ( y and not z )] <true, true, true> =
  Mfact[x](<true, true, true>) OR Mexp[( y and not z )](<true, true, true>) = 
  Mvar1[x](<true, true, true>) OR Mexp[( y and not z )](<true, true, true>) = 
  true OR Mexp[( y and not z )](<true, true, true>) = 
  true OR Mfact[( y and not z )](<true, true, true>) = 
  true OR Mexp[y and not z](<true, true, true>) = 
  true OR (Mfact[y](<true, true, true>) AND Mexp[not z](<true, true, true>)) = 
  true OR (Mvar1[y](<true, true, true>) AND Mexp[not z](<true, true, true>)) = 
  true OR (true AND Mfact[not z](<true, true, true>)) =
  true OR (true AND (NOT Mfact[z](<true, true, true>))) =
  true OR (true AND (NOT Mvar1[z](<true, true, true>))) = 
  true OR (true AND (NOT true)) =
  true OR (true AND false) =
  true OR false =
  true

Razširjeni Boolovi izrazi

Primer 3

Gornjo gramatiko (zgled 1) za Boolove izraze razširimo s prireditvenim in sestavljenim stavkom, tako da je sintaktično pravilen program recimo naslednji:

program
x := true;
y := false;
z := false;
x := x and y;
y := x or (true and (not z))
end

Naloga: Ustrezno definiraj sintakso (v BNF notaciji) ter denotacijsko semantiko programa!

Rešitev:

1. Sintaktična domena (v BNF notaciji)

<prog> ::= program <statements> end
<statements> ::= <var2> ":=" <exp> ";" <statements> | <var2> ":=" <exp> 
<var2> ::= "x" | "y" | "z"

Pozor! <var2> ima enako sintakso kot <var1>, vendar drugačno semantiko!

<exp> ::= <fact> "and" <exp> | <fact> "or" <exp> | <fact>
<fact> ::= "true" | "false" | <var1> | "not" <fact> | ( <exp> )
<var1> ::= "x" | "y" | "z"

2. Opis stanja in semantičnih funkcij

Stanje opisujejo vrednosti spremenljivk x, y in z:

State ≡ {true, false} × {true, false} × {true, false}

Celoten program (posamezen stavek) slika program (posamezen stavek) v funkcijo, ki slika stanje v neko drugo stanje. Spremenljivke x, y in z se lahko skozi program spreminjajo, zato se stanje lahko spreminja:

Mprog: prog -> (State -> State)
Mstatements: statements -> (State -> State)

<var2> preslika ime spremenljivke v njen indeks v stanju:

Mvar2: var2 -> {1, 2, 3}

<exp>, <fact> ter <var1> preslikajo trenutno stanje spremenljivk x, y, in z v vrednost izraza (oz. dejstva ali spremenljivke) true ali false:

Mexp: exp -> (State -> {true, false})
Mfact: fact -> (State -> {true, false})
Mvar1: var1 -> (State -> {true, false})

3. Definicija semantičnih funkcij

Mprog[p: prog](s: State) ≡
  program <statements> end ⇒ Mstatements[p.statements](s)

Mstatements[sts: statements](<sl, s2, s3>: State) ≡
  <var2> := <exp> ; <statements> ⇒ 
    CASE Mvar2[sts.var2] OF
      1 ⇒ Mstatements[sts.statements](<Mexp[sts.exp](s), s2, s3>)
      2 ⇒ Mstatements[sts.statements](<sl, Mexp[sts.exp](s), s3>)
      3 ⇒ Mstatements[sts.statements](<sl, s2, Mexp[sts.exp](s)>)
    END
  <var2> := <exp> ⇒ 
    CASE Mvar2[sts.var2] OF
      1 ⇒ <Mexp[sts.exp](s), s2, s3>
      2 ⇒ <sl, Mexp[sts.exp](s), s3>
      3 ⇒ <sl, s2, Mexp[sts.exp](s)>
    END

Mvar2[v2: var2] ≡ 
  x ⇒ 1 | 
  y ⇒ 2 | 
  z ⇒ 3

Mexp[e: exp](s: State) ≡
  <fact> and <exp> ⇒ Mfact[e.fact](s) AND Mexp[e.exp](s) |
  <fact> or <exp> ⇒ Mfact[e.fact](s) OR Mexp[e.exp](s) |
  <fact> ⇒ Mfact[e.fact](s)

Mfact[f: fact](s: State) ≡
  true ⇒ true |
  false ⇒ false |
  <var1> ⇒ Mvar[f.var1](s) |
  not <fact> ⇒ NOT Mfact[f.fact](s) |
  <exp> ⇒ Mexp[f.exp](s)

Mvar1[v: var1](<xVal, yVal, zVal>: State) ≡
  x ⇒ xVal |
  y ⇒ yVal |
  z ⇒ zVal

Dodaten materijal

• Slika:DenotacijskaSemantika.pdf
• Slika:DenSemPrimer.pdf