Semantika kirjeldamine

Transleerimise viimane etapp on lähteprogrammi interpreteerimine (vahetu täitmine) või väljundkoodi genereerimine hilisemaks (korduvaks) täitmiseks. Tulemus sõltub protsessorist ja operatsioonisüsteemist, mille jaoks translaatorit tehakse. Kuid ühe kindla protsessori ja operatsioonisüsteemi jaoks eraldi translaatori loomine oleks äärmiselt kallis ja ebaotstarbekas, pealegi peaks transleeritud programm kõigis ümbrustes (protsessor+operatsioonisüsteem) töötama ühesuguselt, andma sama tulemuse, s.t. peaks sooritama samasuguse väljundümbruse teisenduse. Sellepärast kirjeldatakse väljundümbrus - milliseid suurusi seal käsitletakse (bitid, baidid, numbrid, märgijadad (stringid) jne) ja milliseid elementaarteisendusi (ühe elementaaroperatsiooniga sooritatavaid) seal saab teha - veidi kõrgemal tasemel kui mingi konkreetse protsessori registrid ja masinkoodid.

Koos teisendatavate suuruste ja kasutatavate elementaarteisendustega peab fikseerima ka transleeritava keele semantika - kuidas iga sisendkäsk seda väljundümbrust muudab. Semantika kirjeldus peab olema matemaatiliselt täpne ja üks-ühene, muidu on võimatu tagada, et erinevate firmade poolt erinevate kasutamisümbruste jaoks loodud translaatorid töötavad ühesuguselt, s.t. transleeritud programmid annavad sama tulemuse. Praktika on näidanud, et transleeritava keele semantika (mida käsud peavad tegema) kirjeldamine loomulikus keeles ei ole kunagi piisavalt täpne, loomulikus keeles esitatud kirjeldustega tekkib alati mitmetimõistmisi. Range, formaalse kirjelduse vajalikkusest nii keele leksika, süntaksi kui ka semantika esitamisel saadi aru juba esimeste programmeerimiskeelte loomisel, kuid just semantika formaalne esitamine on osutunud üsna keerukaks ülesandeks. Näiteks 1960-ndal aastal koostatud programeerimiskeele Algol 60 manualis on keele süntaks juba esitatud Backus-Nauri valemitega (kontekstivaba grammatika); semantika formaalne kirjeldus lubatakse esitada paari kuu pärast, kuid seda pole ilmunud seniajani...

Programmeerimiskeele semantika kirjeldamiseks on kasutatud mitmeid formalisme.

Operatsiooniline semantika (operational semantics) kirjeldab algul (võimalikult lihtsa) "oletatava" arvuti (virtual machine) ja selgitab siis keele konstruktsioone selle virtuaalse arvuti käskudena. Sellisetest virtuaalarvuti keeltest on tuntuim VDL (Vienna Definition Language), firma IBM Viini uurimislaboratooriumis välja töötatud keel, mis loodi programmeerimiskeele PL/1 semantika kirjeldamiseks, ka Java vahekeel JVM on selline.

Kuna operatsiooniline semantika taandab lähtekeele semantika teise programmeerimiskeele (virtuaalse arvuti keele) käskudeks, on see juba oma olemuselt ebatäielik, sest virtuaalarvuti keele täpne tähendus tuleb ikkagi selgitada mitteformaalselt. Rangem ja matemaatilisem semantika kirjeldusviis on nn denotatsiooniline semantika (denotational semantics), mis selgitab käskude toimimist matemaatiliste operatsioonide ja struktuuridega; denotatsioonilise semantika vormis VDM (Vienna Definition Method) on kirjeldatud programmeerimiskeelte Ada, Pascal ja Modula 2 semantika. Matemaatiliselt veel rangem on Hoare ja Wirthi poolt välja töötatud aksiomaatiline semantika, kus programmikäsu S semantika esitatakse induktiivse avaldise {P} S {Q} kujul; siin P ja Q on loogilised predikaadid: P on nn. eeltingimus (precondition) ja Q - järeltingimus ja avaldis {P} S {Q} tähendab, et kui enne käsu S sooritamist kehtis P ja käsk S lõpetas töö vigadeta (alati seda ei juhtu!), siis pärast seda kehtib järeltingimus Q. Kui pärast käsku S sooritatakse käsk S1 ja selle jaoks kehtib {Q}S1{R}, siis võib järeldada, et käskude jada S; S1 jaoks kehtib {P} S; S1 {R}. Kuna eel-ja järeltingimused on loogilised predikaadid, võib järeldusi teha ka loogikareegleid kasutades, kui näiteks P implikatsioon Q ja {Q} S {R}, siis kehtib ka {P} S {R}. Niimoodi samm-sammult eel-ja järeltingimusi kasutades võib arvutada eel-ja järeltingimused kogu programmile P (käskude jada) ja kui programmi P spetsifikatsioon (s.t. mida see peab tegema) on samuti esitatud loogiliste predikaatidena, saab kogu programmi tõestada - kontrollida, et P eel- ja järeltingimused rahuldavad spetsifikatsiooni. See on küll matemaatiliselt range, kuid väga ebapraktiline ja isegi lihtsate programmide fomaalne tõestus tuleb väga pikk ja keeruline, näiteks programmeerimiskeele Modula 2 kirjelduse (mitteformaalse ja kohati mitmetimõistetava) kirjelduse esitas Wirth kolmekümne viiel leheküljel, kuid keele formaalne semantika kirjeldus tuli rohkem kui 700 lehekülge.

Semantika kirjeldamiseks kasutatakse ka attribuutgrammatikaid. Näiteks Ada semantika kirjeldamiseks loodi Karlsruhe Ülikooli Informaatikainstituudis attribuutgrammatika AG; Ada semantika kirjelduse maht on 511 lk ja see on üsna raskesti loetav ja arusaadav, järgnevas on paar juhuslikult võetud rida (funktsiooni attribuudi väärtustamise reeglite algus; ka siin kasutatakse eel- ja järeltingimusi):

 FUNCTION f_attr_constrained (p_obj : tp_descr_set,
p_env : tp_env) tp_descr_set:
f_descr_set_val
(c_bool_constr,
IF (f_obj_constraint (p_obj) /= sc_void)
OR (f_head_descr (p_obj).s_nature = sc_in)
THEN IF ...

Praktikas kasutatakse semantika kirjeldamiseks tavaliselt vaid mingit väga lihtsat objektkeelt või lihtsa struktuuriga virtuaalmasina keelt, millest eeldatakse, et selle toimimine on üheselt mõistetav. Selline on näiteks nn kolmeaadressiline kood (three-address code). Kolmeaadressilise koodi käsud on üsna sarnased tavalise imperatiivse programmeerimiskeele käskudega, kuid omistamislause paremal pool võib kasutada vaid üht operatsiooni, seega omistamiskäsus võib (maksimaalselt) olla kolm muutujat - muutuja vasakul (millele omistatakse) ka kaks operandi paremal (kuid muutujaid võib olla ka vähem) - siit ka nimi.

Oma töödega on D.Knuth saanud (pool)jumala aupaiste, mida hästi iseloomustab järgnev anekdoot: "Richard M. Stallman (vaba tarkvara organisatsiooni ja editori Emacx looja), Linus Thorvalds ja Donald E. Knuth vestlesid kord sellest, kelle panus programmeerimisse on olnud suurim.
Stallman: "Jumal ütles mulle, et ma olen programmeerinud maailma parima editori!"
Thorvalds: "Aga mulle ütles jumal, et ma olen programmeerinud maailma parima operatsioonisüsteemi!"
Knuth: "Pidage, pidage- ma pole kunagi midagi sellist öelnud!"

Paljude dissertatsioonide ja artiklite tulemusena on esitatud mitmesuguseid rangeid semantika matemaatilisi kirjeldusmeetodeid. Enamasti on need väga ranged (matemaatilised), kuid üsna raskesti arusaadavad ja sageli algavad täiesti uue matemaatilise formalismi defineerimisega, sest autor kas pole suutnud olemasolevaid formalisme läbi seedida või arvab, et kõik, mis on enne teda tehtud, on jamps. Tavaprogrammeerijad neid peaaegu ei loe, pealegi ei välista nende kasutamine vigu. Me (inimesed) saame väga halvasti aru ajas toimuvatest protsessidest, s.t. mis programmi käivitamise järel tegelikult juhtuma hakkab, ükskõik kui põhjalikult me programmi matemaatiliselt ka ei analüüsiks - aga see ongi imperatiivsetes (käsu-) keeltes programmerimise kõige raskem - näha ette kõike, mis juhtuma hakkab (funktsionaalsetes ja loogilistes keeltes seda probleemi peaaegu pole, sest seal me tegeleme konseptuaalse analüüsiga - milline on probleemi sisu/struktuur) . Tõestus inimeste väga kehvale ajas toimuvate protsesside ettenägemisele on kasvõi viimase viiekümne aasta kõige grandioossema ja kõige rohkem inimesi muserdanud eksperimendi (kommunism) - läbikukkumine - teoorias on kõik kena, kuid teooria ei suutnud ette näha, mis tegelikult juhtuma hakkab. Paljud lääne noored, kes seda (kommunismi) lähedalt näinudki pole, arvavad, et viga oli vaid realisatsioonis, umbes nii et täisarvudele oleks pidanud reserveerima mitte 32 bitti, vaid 64 - siis oleks arvutustäpsus olnud kahekordne ... - annaks Jumal (kui Ta on olemas), et me järgmise viiekümne aasta pärast taas ei istuks lõhkise küna ees (aga siis eestlasi vist peaaegu enam ei ole...).

D. Knuth iseloomustas programmeerimist kui kunsti: "Computer programming is an art form, like the creation of poetry or music". Kuid kunsti ei saa (praegused arvutid veel ei suuda) matemaatiliselt tõestada. Knuth saatis ükskord kirjas programmi, millele ta oli lisanud selle korrektsuse pika tõestuse, kuid programmi formaalse tõestuse lõppu lisas ta: "Beware of bugs in the above code; I have only proved it correct, not tried it." - isegi Knuth-i arvates formaalne tõestus ei välista, et programm tegelikult teeb seda, milleks ta on kirjutatud; programmi korrektsuse üle otsustab vaid arvuti. Täpselt samuti otsustab filosioofiliste doktriinide ja poliitiliste parteide poliitika üle vaid ajalugu - mis sellest siis 10 - 50 - 100 aasta pärast välja tuli ?

 


Ülesandeid:
1. Ylesande tekst
Ksimused, probleemid: ©2004 Jaak Henno