Back

ⓘ Семантика програмских језика




                                     

ⓘ Семантика програмских језика

У теорији програмских језика, семантика је област која се бави строгим математичким проучавањем значења програмских језика. Она придружује значење синтаксно исправним стринговима. Семантика описује процес извршавања програма на неком одређеном програмском језику. То може да се уради било описивањем везе између улаза и излаза програма, било објашњењем тога како ће програм бити извршен на одређеној платформи, то јест креирањем модела израчунавања.

Улога семантике:

  • разумевање карактеристика програмског језика и њихове интеракције
  • доказивање својстава одређеног програмског језика
  • програмер може да разуме како се програм извршава пре његовог покретања као и шта мора да обезбеди приликом креирања компилатора

Семантика може да се опише формално и неформално. На пример, формална семантика олакшава писање компилатора, боље разумевање тога шта програм ради као и доказивање на пример тога да следећа наредба:

if 1 = 1 then S1 else S2

има исти ефекат као само S1.

                                     

1. Преглед

Област формалне семантике обухвата следеће теме:

  • веза имеђу израчунавања и основних математичких структура које стоје иза тога, на пример из области логике, теорије скупова, теорије модела, теорије категорија итд.
  • дефиниција семантичких модела
  • веза између различитих семантичких модела
  • веза између различитих приступа значењу

Уско је повезана и са другим областима рачунарства и информатике попут дизајна програмских језика, компилирања, интерпретирања, верификације програма.

                                     

2. Статичка семантика

Статичка семантика дефинише ограничења на структуре валидних текстова које је тешко или немогуће изразити користећи стандардне синтатичке формализме. За језике који се компилирају, статичка семантика обухвата она семантичка правила која се могу проверити у току компилације. На пример, провера да ли је сваки идентификатор декларисан пре употребе у оним програмским језицима који захтевају декларацију пре употребе или да су ознаке у case наредби различите. Многа важна ограничења овог типа, попут провере тога да ли су идентификатори употребљени у исправном контексту нпр. не додајемо цео број имену функције или да позиви у подрутинама имају одговарајући број и тип аргумената, се могу остварити тако што ћемо их дефинисати као правила у логици која се зове систем типова.

                                     

3. Семантички модели

Појмови попут семантичке мреже и семантичког дата модела се користе за описивање посебних типова дата модела које карактерише употреба директних графова у којима темена означавају концепте или ентитете у свету, а лукови означавају везе између њих. Семантички веб представља екстензију светске мреже која настаје уграђивањем семантичких метаподатака коришћењем техника семантичког дата моделовања попут RDF-a и OWL-а.

                                     

4. Подела

  • Операциона семантика
  • Аксиоматска семантика
  • Денотациона семантика

Приступи

Gordon Plotkin је увео структурну операциону семантику, Robert Hieb и Matthias Felleisen контекст смањења, и Gilles Kahn природну семантику.

Денотациона семантика недетерминистичких програма

Концепт моћи домена је развијен да омогући денотациону семантику недетерминистичким секвенцијалним програмима.

                                     

4.1. Подела Аксиоматска семантика

Аксиоматска семантика је једна врста приступа заснована на математичкој логици која служи за доказивање коректности рачунарског програма. Она дефинише значење команди у програму тако што описује њихов ефекат на наредбе везане за стање рачунарског програма. Значење рачунарског програма није експлицитнно дато, већ су својства језичких контруката дефинисана преко аксиома и правила инференције симболичке логике. Својство програма је изведено из њих да би се конструисао формалан доказ својства. Дакле, аксиоматска семантика нам не даје директно значење програма, већ оно што може бити доказано о програму. Постоје две врсте примене: верификација програма и спецификација семантике програма.

Кључна идеја је да се не дефинише понашање програма као операционом или денотационом семантиком и извоћење из тих дефиниција, већ се узимају сами закони тих дефиниција. Значење термина је оно што може бити доказано о њему. Лепота аксиоматских метода јесте што се фокусирају на процес закључивања, процес који је у рачунарству довео до великих идеја попут инваријанти.

Једноставни системи могу нпр. подржати доказе да је један програм еквивалентан другом, које год значење имали. Сложенији системи могу подржавати и доказе о улазно/излазним својствима програма. Аксиоматске дефиниције су апстрактније од денотационих и операционих, тако да својства доказана о програму можда не буду довољна да у потпуности одреде значење програма. Ова врста формата је најбоља за прелиминарне спецификације језика, као и за достављање документације о занимљивим својствима језика корисницима.



                                     

4.2. Подела Тврдње

Логичке изразе који се јављају у аксиоматској семантици зовемо предикати, односно тврдње. Они описују ограничења програмских променљивих. Постоје две врсте тврдњи: предуслов и постуслов. Аксиоматска семантика има за основу математичку логику, на пример Хорову логику. Хорова тројка {P} C {Q} описује како извршавање дела кода мења стање израчунавања; ако је испуњен предуслов {P}, извршавање команде C води до постуслова {Q}. Хорова логика обезбеђује аксиоме и правила извођења за све консртукте једноставног императивног програмског језика. Пример за постусловну тврдњу: sum = 2 * x + 1 {sum > 1}.

Једна од могућности за предусловну тврдњу везану за овај израз била би: {x > 10}.

                                     

4.3. Подела Најслабији предуслов

Најслабији предуслов је најмањи рестриктивни предуслов који ће гарантовати валидност повезаног постуслова. У претходном примеру {x > 10}, {x > 50} и {x > 1000} су све валидни предуслови, али {x > 0} је најслабији предуслов. Правило закључивања је метод да истинитост једне тврдње нађемо на основу истинитости других тврдњи. Општи облик правила изгледа овако:

S 1, S 2., S n S {\displaystyle {\frac {S_{1},S_{2}.,S_{n}}{S}}}

Ово правило каже да ако су S 1, S 2., S n истинити онда можемо закључити и о истинитости тврдње S. Горњи део правила се зове претходник, а доњи доследник.

Најслабији предуслов за секвенцу изјава не може се описати аксиомом, јер предуслов зависи од посебних изјава у секвенци. У том случају, предуслов се може описати само помоћу правила закључивања. Нека су S1 и S2 две упоредне програмске изјаве. Ако S1 и S2 имају следеће предуслове и постуслове: {P1} S1 {P2}, {P2} S2 {P3}, онда правило закључивања ове секције гласи:

{ P 1 } S 1 { P 2 }, { P 2 } S 2 { P 3 } { P 1 } S 1, S 2 { P 3 } {\displaystyle {\frac {\{P1\}S1\{P2\},\{P2\}S2\{P3\}}{\{P1\}S1,S2\{P3\}}}}

Дакле, за овај пример, {P1} S1; S2 {P3} описује аксиоматску семантику секвенце S1; S2.

Правило извођења селекције чији је општи облик if B then S1 else S2 је:

{ B and P } S 1 { Q }, { not B and P } S 2 { Q } { P } if B then S 1 else S 2 { Q } {\displaystyle {\frac {\{B{\mbox{ and }}P\}S1\{Q\},\{{\mbox{not }}B{\mbox{ and }}P\}S2\{Q\}}{\{P\}{\mbox{ if }}B{\mbox{ then }}S1{\mbox{ else }}S2{\mbox{ }}\{Q\}}}}

Ово правило указује на то да изјава мора бити доказана и када је логичка вредност израза тачна и када је нетачна. Према правилу, треба нам предуслов P који може бити употребљен као предуслов и then и else клаузуле. Уколико B испуњава предуслов, онда ће се извршити then грана, а уколико не испуњава извршиће се else грана.

Још једна есенцијална конструкција императивних језика јесте while петља. Рачунање најслабијег предуслова за while петљу је знатно теже него за секвенце, зато што број итерација не може увек бити одређен. Проблем рачунања најслабијег предуслова за петље је сличан проблему доказивања теореме о природним бројевима. Први корак је пронаћи инваријанту петље, која је кључна за проналазак најслабијег предуслова. Правило закључивања гласи:

{ I and B } S { I } { I } while B do S end { I not B } {\displaystyle {\frac {\{I{\mbox{ and }}B\}S\{I\}}{\{I\}{\mbox{ while }}B{\mbox{ do }}S{\mbox{ end }}\{I{\mbox{ not }}B{\mbox{}}\}}}}

I је инваријанта петље. Иако делује лако, није ни мало тако. Комплексност лежи у проналаску одговарајуће инваријанте петље. Аксиоматски опис while петље гласи:

{P} while B do S end {Q}.


                                     

4.4. Подела Операциона семантика

Операциона семантика је категорија формалне семантике програмских језика у којој одређена жељена својства програма, као што су тачност, сигурност и безбедност, су верификована изградњом доказа из логичких изјава о њиховом извршењу и процедурама, а не везивањем математичког значења са њеним условима денотациона семантика. Операциона семантика је класификована у две категорије: структурна операциона семантика формално која описује како поједини кораци у израчунавању утичу на систем компјутера, док природна семантика описују како се добијају крајњи резултати извршења. Остали приступи формалној семантици програмских језика укључују аксиоматску семантику и денотациону семантику.

Операциона семантика програмских језика описује како се исправан програм тумачи као низ рачунарских корака. Овај низ корака представља значење програма. У функционалном програмирању, завршни корак у низу враћа вредност програма.

Концепт операционе семантике је коришћен први пут у дефинисању семантике Алгол 68. Следећа изјава је прерађени цитат иѕ АЛГОЛ 68 иѕвештаја:

Значење програма у строгом језику је објашњен преко хипотетичког рачунара који врши низ акција које чине израду тог програма. Алгол68, Одељак 2

Прва употреба термина операциона семантика у свом садашњем смислу се приписује Dana Scott-a. Оно што следи је цитат из Скотових папира о формалној семантици, у којој се помињу "операциони" аспекти семантике.

То је све веома добро да тежи више апстрактно и на чистији приступ семантици, али ако је у плану да буде добро у било ком смислу, операциони аспекти не могу се у потпуности игнорисати.

Можда је прво формално оличење оперативне семантике употреба ламбда рачуна за дефинисање семантике ЛИСП-а од стране Џона Макартија.

                                     

4.5. Подела Приступи

Gordon Plotkin је увео структурну операциону семантику, Robert Hieb и Matthias Felleisen контекст смањења, и Gilles Kahn природну семантику.

                                     

4.6. Подела Структурна операциона семантика

Структурну операциону семантику је увео Gordon Plotkin као логичан начин да се дефинише операциона семантика. Основна идеја иза СОС је да дефинише понашање програма у погледу понашања његових делова, чиме се обезбеђује структурни, то јест, синтаксно оријентисан и индуктивни, поглед на оперативну семантику. СОС спецификација дефинише понашање програма у смислу транзиције односа. СОС спецификације су у форми низа правила која дефинишу валидне транзиције од делова синтаксе у смислу транзиције његових компоненти.

Таква дефиниција омогућава формалну анализу понашања програма, дозвољавајући проучавање односа између програма. Важни односи укључују симулације унапред и бисимулацију. Они су нарочито корисни у контексту теорије конкуренције.

Захваљујући својим интуитивним изгледима и структури која се лако прати, СОС је стекао велику популарност и постао стандард у пракси у дефинисању оперативне семантике. Као знак успеха, оригинални извештај тзв Архус извештај на СОС Плоткин81 је привукао више од 1000 цитата у складу са CiteSeer., што га чини једним од највећих наведених техничких извештаја у информатици.



                                     

4.7. Подела Редукциона семантика

Редукциона семантика је алтернативан вид операционе семантике помоћу такозваних контекста смањење. Методу је увео Robert Hieb и Matthias Felleisen 1992. године као техника за формализовање опште теорије алгебре за управљање током и стањима. На пример, граматика позива по вредности ламбда рачуна и њени контексти могу бити задати као:

e = v | e | x v = λ x. e C = }

Најмања горња граница овог ланца је цела factorial функција која се може изразити помоћу симбола "⊔" који представља "најмање горње ограничење":

⨆ i ∈ N F i { }. {\displaystyle \bigsqcup _{i\in \mathbb {N} }F^{i}\{\}.}
                                     

4.8. Подела Денотациона семантика недетерминистичких програма

Концепт моћи домена је развијен да омогући денотациону семантику недетерминистичким секвенцијалним програмима.

                                     

4.9. Подела Принцип композиције

Битан аспект денотационе семантике програмског језика је принцип композиције, денотација програма је изграђена од денотација његових делова. На пример, посматрајмо израз "7 + 4". Принцип композиције у овом слуачају обезбеђује значење за "7 + 4" у складу са значењима од "7", "4" и "+".

Основа денотационе семантике у теоријском домену задовољава принцип композиције јер је задата на следећи начин. Почињемо тако што посматрамо фрагмент програма, тј. програм са слободним промењивима. Контекст за куцање додељује тип слободним промењивим. На пример, у изразу x + y може се посматрати у контексту куцања x: nat, y: nat. Денотациону семантику додељујемо програмском фрагменту користећи следећу шему.

  • Коначно, морамо да дамо значење сваком програмском фраменту. Претпоставимо да је P програмски фрагмент типа σ, у контексту куцања Γ, најчешће у ознаци Γ⊢ P:σ. Онда значење овог програмског фрагмента мора бити непрекидна функција〚Γ⊢ P:σ〛:〚Γ〛→〚σ〛. На пример, 〚⊢7: nat 〛:1→ℕ ⊥ је константна функција, која увек има вредност "7", док 〚 x: nat, y: nat ⊢ x + y: nat 〛:ℕ ⊥ ×ℕ ⊥ →ℕ ⊥ је функција која сабира два броја.
  • Почињемо тако што описујемо значење типова у нашем језику: значење сваког типа мора да буде домен. Пишемо〚τ〛 за домен који означава врсту τ. На пример, значење типа nat треба да буде домен природних бројева: 〚 nat 〛= ℕ ⊥.
  • Из значења типова изводимо значење за контекст куцања. Поставимо 〚 x 1:τ 1., x n:τ n 〛 = 〚 τ 1 〛×. ×〚τ n 〛. На пример, 〚 x: nat, y: nat 〛= ℕ ⊥ ×ℕ ⊥. Као специјалан случај, значење празног контекста за куцање, без промењивих, је домен са једним елементом, и означава 1.

Сада, значење израза 7+4 је одређено са три израза 〚⊢7: nat 〛:1→ℕ ⊥, 〚⊢4: nat 〛:1→ℕ ⊥, и〚 x: nat, y: nat ⊢ x + y: nat 〛:ℕ ⊥ ×ℕ ⊥ →ℕ ⊥.

У ствари, ово је уопштена шема за денотациону семантику која се заснива на композицији. Нема ништа специфично у вези са доменима и непрекидним функцијама овде.