Metateorija programskih jezikov

Metateorija programskih jezikov#

Vsak programski jezik ima svojo teorijo, torej pravila, ki formalno opisujejo, kako se programi izvajajo ali določajo, katere programe smatramo za veljavne. Od teorije so odvisne lastnosti programskega jezika, na primer to, da se veljavni programi lahko vedno uspešno izvedejo, ali pa to, da je rezultat enolično določen. Lastnostim programskega jezika, ki sledijo iz dane teorije, pravimo metateorija. Za primer si oglejmo že znani programski jezik IMP.

Teorija#

Sintaksa#

Del teorije IMPa smo že srečali, in sicer njegovo abstraktno sintakso, ki jo tu le ponovimo:

\begin{array}{r} \begin{aligned} aritmetični izraz e & ::= ℓ ∣ \underset{―}{n} ∣ e_{1} + e_{2} ∣ e_{1} - e_{2} ∣ e_{1} * e_{2} \\ logični izraz b & ::= true ∣ false ∣ e_{1} = e_{2} ∣ e_{1} < e_{2} ∣ e_{1} > e_{2} \\ ukaz c & ::= if b then c_{1} else c_{2} ∣ while b do c ∣ c_{1}; c_{2} ∣ ℓ := e ∣ skip \end{aligned} \end{array}

Operacijska semantika#

V sintaksi uporabljamo besede in simbole, ki nakazujejo na pomen posameznih izrazov in ukazov, ampak to pomena formalno ne podaja. Najprej podajmo dinamično oziroma operacijsko semantiko, ki določa, kako se programi izvajajo. To smo enkrat že storili prek programa v OCamlu, zdaj pa to storimo še v jeziku matematike.

Začnimo z aritmetičnimi izrazi, ki naj bi predstavljali cela števila. Ker v aritmetičnih izrazih lahko dostopamo do lokacij $ℓ$ , moramo pomen podati relativno na neko stanje, ki ga predstavimo z množico parov lokacij in prirejenih vrednosti ${ℓ_{1} \mapsto n_{1}, \dots, ℓ_{k} \mapsto n_{k}}$ . Tromestno relacijo $s, e ⇓ n$ , ki pove, da izraz $e$ v stanju $s$ predstavlja število $n$ , podamo kot najmanjšo relacijo, zaprto za sledeča pravila:

\begin{array}{r} \frac{(ℓ \mapsto n) \in s}{s, ℓ ⇓ n} \frac{}{s, \underset{―}{n} ⇓ n} \\ \frac{s, e_{1} ⇓ n_{1} s, e_{2} ⇓ n_{2}}{s, (e_{1} + e_{2}) ⇓ (n_{1} + n_{2})} \frac{s, e_{1} ⇓ n_{1} s, e_{2} ⇓ n_{2}}{s, (e_{1} - e_{2}) ⇓ (n_{1} - n_{2})} \frac{s, e_{1} ⇓ n_{1} s, e_{2} ⇓ n_{2}}{s, (e_{1} * e_{2}) ⇓ (n_{1} \cdot n_{2})} \end{array}

Na primer, za stanje $s = {ℓ \mapsto 6, m \mapsto - 5}$ velja $s, ℓ * (\underset{―}{3} + \underset{―}{4}) ⇓ 42$ , saj imamo sledeče drevo izpeljave:

\frac{\frac{(ℓ \mapsto 6) \in s}{s, ℓ ⇓ 6} \frac{\frac{}{s, \underset{―}{3} ⇓ 3} \frac{}{s, \underset{―}{4} ⇓ 4}}{s, (\underset{―}{3} + \underset{―}{4}) ⇓ 7}}{s, ℓ * (\underset{―}{3} + \underset{―}{4}) ⇓ 42}

Če aritmetični izraz $e$ vsebuje dostop do lokacije $ℓ$ , ki v stanju $s$ ni nastavljena, bi to v implementaciji sprožilo napako ob izvajanju, v matematični formulaciji pa preprosto pomeni, da za nobeno število $n$ ne velja $s, e ⇓ n$ .

Podobno podamo relacijo $s, b ⇓ r$ , ki pove, kdaj logični izraz $b$ v danem stanju $s$ predstavlja resničnostno vrednost $r \in B = {t t, f f}$ :

\begin{array}{r} \frac{}{s, true ⇓ t t} \frac{}{s, false ⇓ f f} \\ \frac{s, e_{1} ⇓ n_{1} s, e_{2} ⇓ n_{2} n_{1} = n_{2}}{s, (e_{1} = e_{2}) ⇓ t t} \frac{s, e_{1} ⇓ n_{1} s, e_{2} ⇓ n_{2} n_{1} \neq n_{2}}{s, (e_{1} = e_{2}) ⇓ f f} \\ \frac{s, e_{1} ⇓ n_{1} s, e_{2} ⇓ n_{2} n_{1} < n_{2}}{s, (e_{1} < e_{2}) ⇓ t t} \frac{s, e_{1} ⇓ n_{1} s, e_{2} ⇓ n_{2} n_{1} \geq n_{2}}{s, (e_{1} < e_{2}) ⇓ f f} \\ \frac{s, e_{1} ⇓ n_{1} s, e_{2} ⇓ n_{2} n_{1} > n_{2}}{s, (e_{1} > e_{2}) ⇓ t t} \frac{s, e_{1} ⇓ n_{1} s, e_{2} ⇓ n_{2} n_{1} \leq n_{2}}{s, (e_{1} > e_{2}) ⇓ f f} \end{array}

Pri ukazih so pravila malo drugačna, saj za razliko od izrazov ne predstavljajo nobenih vrednosti, temveč je njihov končni rezultat spremenjeno stanje. Poleg tega se zaradi morebitnih neskončnih zank izvajanje ukazov ne konča vedno. Zaradi slednjega bomo pomen ukazov podali prek semantike malih korakov $s, c ⇝ s^{'}, c^{'}$ , ki ukaza $c$ v stanju $s$ ne bo povezala s končnim rezultatom, temveč z novim ukazom $c^{'}$ in novim stanjem $s^{'}$ , ki predstavljata spremembe, ki so se zgodile v enem računskem koraku.

\begin{array}{r} \frac{s, b ⇓ t t}{s, if b then c_{1} else c_{2} ⇝ s, c_{1}} \frac{s, b ⇓ f f}{s, if b then c_{1} else c_{2} ⇝ s, c_{2}} \\ \frac{s, b ⇓ t t}{s, while b do c ⇝ s, (c; while b do c)} \frac{s, b ⇓ f f}{s, while b do c ⇝ s, skip} \\ \frac{s, c_{1} ⇝ s^{'}, c_{1}^{'}}{s, (c_{1}; c_{2}) ⇝ s^{'}, (c_{1}^{'}; c_{2})} \frac{}{s, (skip; c_{2}) ⇝ s, c_{2}} \\ \frac{s, e ⇓ n}{s, ℓ := e ⇝ s [ℓ \mapsto n], skip} \end{array}

Vidimo, da takrat, kadar pogoj v logičnem ukazu predstavlja resnico, v naslednjem računskem koraku začnemo izvajati prvo, sicer pa drugo vejo, obe v nespremenjenem stanju. Podobno ločimo dva primera pri zankah. Če je pogoj resničen, izvedemo telo, ki mu sledi še ena ponovitev zanke, sicer pa zaključimo izvajanje. Pri zaporednem izvajanju korak naredimo v prvem ukazu in ustrezno spremenimo stanje. Če je prvi ukaz končal z izvajanjem, začnemo izvajati drugi ukaz. Pri prirejanju spremenimo stanje in zaključimo izvajanje. Ukaz $skip$ predstavlja zaključeno izvajanje, zato pravila zanj nimamo.

S tako podanimi pravili lahko pokažemo, da je semantika ukazov deterministična. Če velja tako $s, c ⇝ s^{'}, c^{'}$ kot $s, c ⇝ s^{″}, c^{″}$ , tedaj je $s^{'} = s^{″}$ in $c^{'} = c^{″}$ . Dokaz poteka z indukcijo, pri tem pa si pomagamo s pomožnima trditvama, da sta tudi semantiki aritmetičnih in logičnih izrazov deterministični.

Določanje veljavnih programov#

Želeli bi pokazati, da vsak program lahko vedno naredi korak, vendar to ni res, saj lahko nekateri programi dostopajo do lokacij, ki v stanju niso nastavljene. Da bi se tem primerom izognili, smo v implementaciji napisali funkcijo check, ki je program preverila, preden ga je začela izvajati. Matematično pa bomo to zopet podali z induktivnimi relacijami. Relacijo $L ⊢ e$ , ki podaja, kdaj aritmetični izraz $e$ dostopa le do lokacij iz množice $L$ , podamo s sledečimi pravili:

\begin{array}{r} \frac{ℓ \in L}{L ⊢ ℓ} \frac{}{L ⊢ \underset{―}{n}} \\ \frac{L ⊢ e_{1} L ⊢ e_{2}}{L ⊢ (e_{1} + e_{2})} \frac{L ⊢ e_{1} L ⊢ e_{2}}{L ⊢ (e_{1} - e_{2})} \frac{L ⊢ e_{1} L ⊢ e_{2}}{L ⊢ (e_{1} * e_{2})} \end{array}

Podobno to storimo za logične izraze:

\begin{array}{r} \frac{}{L ⊢ true} \frac{}{L ⊢ false} \\ \frac{L ⊢ e_{1} L ⊢ e_{2}}{L ⊢ (e_{1} = e_{2})} \frac{L ⊢ e_{1} L ⊢ e_{2}}{L ⊢ (e_{1} < e_{2})} \frac{L ⊢ e_{1} L ⊢ e_{2}}{L ⊢ (e_{1} > e_{2})} \end{array}

Pri ukazih je situacija malenkostno drugačna, saj spreminjajo stanje in s tem tudi množico veljavnih lokacij. Tako podamo relacijo $L ⊢ c, L^{'}$ , ki pove, da ukaz $c$ dostopa le do lokacij iz množice $L$ , po izvajanju pa bodo definirane vse lokacije iz množice $L^{'}$ .

\begin{array}{r} \frac{L ⊢ b L ⊢ c_{1}, L_{1} L ⊢ c_{2}, L_{2}}{L ⊢ if b then c_{1} else c_{2}, L_{1} \cap L_{2}} \frac{L ⊢ b L ⊢ c, L^{'}}{L ⊢ while b do c, L^{'}} \\ \frac{L ⊢ c_{1}, L^{'} L^{'} ⊢ c_{2}, L^{″}}{L ⊢ (c_{1}; c_{2}), L^{″}} \frac{L ⊢ e}{L ⊢ ℓ := e, L \cup {ℓ}} \frac{}{L ⊢ skip, L} \end{array}

Izrek o varnosti#

Eden glavnih izrekov, ki jih običajno dokažemo, ko obravnavamo metateorijo programskega jezika, je izrek o varnosti. Ta govori o tem, da se veljavni programi lahko uspešno izvedejo. Razdeljen je na dva dela:

napredek, ki pove, da veljaven program bodisi lahko naredi še en računski korak bodisi je uspešno zaključil izvajanje,
ohranitev, ki pove, da veljaven program po enem računskem koraku ostane veljaven.

Oba skupaj povesta, da vsak veljaven program izvaja računske korake do točke, ko zaključi izvajanje, ali pa teče v neskončnost. Oglejmo si vsakega posebej.

Napredek#

Naj bo $s$ stanje, definirano na vseh lokacijah iz množice $L$ . Tedaj:

Za vsak aritmetični izraz $e$ , za katerega velja $L ⊢ e$ , obstaja $n \in Z$ , da velja $s, e ⇓ n$ .
Za vsak logični izraz $b$ , za katerega velja $L ⊢ b$ , obstaja $r \in B$ , da velja $s, b ⇓ r$ .
Za vsak ukaz $c$ in množico lokacij $L^{'}$ , za katera velja $L ⊢ c, L^{'}$ :
1. bodisi obstajata ukaz $c^{'}$ in stanje $s^{'}$ , da velja $s, c ⇝ s^{'}, c^{'}$ ,
2. bodisi velja $c = skip$ .

Dokaz#

Vsak del dokažemo z indukcijo.

Obravnavajmo vsa pravila, po katerih smo lahko prišli do zaključka $L ⊢ e$ .
- Če smo uporabili pravilo $\frac{ℓ \in L}{L ⊢ ℓ}$ , potem je $ℓ \in L$ , torej po predpostavki obstaja $n$ , da velja $(ℓ \mapsto n) \in s$ , zato velja tudi $s, ℓ ⇓ n$ .
- Če smo uporabili pravilo $\frac{}{L ⊢ \underset{―}{n}}$ , potem velja $s, \underset{―}{n} ⇓ n$ .
- Če smo uporabili pravilo $\frac{L ⊢ e_{1} L ⊢ e_{2}}{L ⊢ (e_{1} + e_{2})}$ , potem po indukcijski predpostavki obstajata $n_{1}$ in $n_{2}$ , da velja $s, e_{1} ⇓ n_{1}$ in $s, e_{2} ⇓ n_{2}$ . Tedaj velja tudi $s, (e_{1} + e_{2}) ⇓ (n_{1} + n_{2})$ . Podoben dokaz uporabimo še v primerih $L ⊢ (e_{1} - e_{2})$ in $L ⊢ (e_{1} * e_{2})$ .
Obravnavajmo vsa pravila, po katerih smo lahko prišli do zaključka $L ⊢ b$ .
- Če smo uporabili pravilo $\frac{}{L ⊢ true}$ , potem velja $s, true ⇓ t t$ . Podoben dokaz uporabimo še v primeru $L ⊢ false$ .
- Če smo uporabili pravilo $\frac{L ⊢ e_{1} L ⊢ e_{2}}{L ⊢ (e_{1} = e_{2})}$ , potem po poprej dokazani trditvi obstajata $n_{1}$ in $n_{2}$ , da velja $s, e_{1} ⇓ n_{1}$ in $s, e_{2} ⇓ n_{2}$ . Ker velja bodisi $n_{1} = n_{2}$ bodisi $n_{1} \neq n_{2}$ , vedno obstaja $r \in B$ , da velja $s, (e_{1} = e_{2}) ⇓ r$ . Podoben dokaz uporabimo še v primerih $L ⊢ (e_{1} < e_{2})$ in $L ⊢ (e_{1} > e_{2})$ .
Obravnavajmo vsa pravila, po katerih smo lahko prišli do zaključka $L ⊢ c, L^{'}$ .
- Če smo uporabili pravilo $\frac{L ⊢ b L ⊢ c_{1}, L_{1} L ⊢ c_{2}, L_{2}}{L ⊢ if b then c_{1} else c_{2}, L_{1} \cap L_{2}}$ , potem po prejšnji trditvi obstaja $r \in B$ , da velja $s, b ⇓ r$ . Če je $r = t t$ , potem velja $c, s ⇝ c_{1}, s$ , če pa je $r = f f$ , pa velja $c, s ⇝ c_{2}, s$ . V obeh primerih torej lahko naredimo korak.
- Podoben dokaz lahko naredimo v primeru $L ⊢ while b do c, L^{'}$ .
- Če smo uporabili pravilo $\frac{L ⊢ c_{1}, L^{'} L^{'} ⊢ c_{2}, L^{″}}{L ⊢ (c_{1}; c_{2}), L^{″}}$ , po indukcijski predpostavki za $L ⊢ c_{1}$ velja:
  1. bodisi obstajata ukaz $c_{1}^{'}$ in stanje $s^{'}$ , da velja $s, c_{1} ⇝ s^{'}, c_{1}^{'}$ , zaradi česar velja tudi $s, (c_{1}; c_{2}) ⇝ s^{'}, (c_{1}^{'}; c_{2})$ ,
  2. bodisi je $c_{1} = skip$ , zaradi česar velja $s, (skip; c_{2}) ⇝ s, c_{2}$ .
  V obeh primerih torej lahko naredimo korak.
- Če smo uporabili pravilo $\frac{L ⊢ e}{L ⊢ ℓ := e, L \cup {ℓ}}$ , potem po prejšnji trditvi obstaja $n$ , da velja $s, e ⇓ n$ , zato velja tudi $s, (ℓ := e) ⇝ s [ℓ \mapsto n], skip$ .
- Če smo uporabili pravilo $\frac{}{L ⊢ skip, L}$ , potem velja $c = skip$ .

Opazimo lahko, da v dokazu napredka za ukaze ne uporabimo druge množice lokacij $L^{'}$ . Ta pride v poštev, če želimo narediti več kot en korak.

Varnost#

Vzemimo ukaza $c, c^{'}$ , množici lokacij $L, L^{'}$ ter stanji $s, s^{'}$ , tako da:

je stanje $s$ definirano na vseh lokacijah iz množice $L$ ,
velja $L ⊢ c, L^{'}$ , ter
velja $s, c ⇝ s^{'}, c^{'}$ .

Tedaj obstaja množica lokacij $L^{″}$ , da velja $L^{″} ⊢ c^{'}, L^{'}$ in je $s^{'}$ definirano na vseh lokacijah iz množice $L^{″}$ .

Pozorni bodimo na dejstvo, da množica lokacij $L^{'}$ ne ustreza stanju $s^{'}$ , saj gre za množico lokacij po koncu izvajanja ukaza $c$ , med tem ko se je v $s^{'}$ lahko v enem samem koraku spremenila le ena. Na primer, velja $\emptyset ⊢ (ℓ := \underset{―}{3}; m := \underset{―}{4}), {ℓ, m}$ in $\emptyset, (ℓ := \underset{―}{3}; m := \underset{―}{4}) ⇝ {ℓ \mapsto 3}, (skip; m := \underset{―}{4})$ . V tem primeru je $L = \emptyset$ , $L^{'} = {ℓ, m}$ ter $L^{″} = {ℓ}$ .