У теорији програмских језика, семантика је област која се бави строгим математичким проучавањем значења програмских језика. Она придружује значење синтаксно исправним стринговима. Семантика описује процес извршавања програма на неком одређеном програмском језику. То може да се уради било описивањем везе између улаза и излаза програма, било објашњењем тога како ће програм бити извршен на одређеној платформи, то јест креирањем модела израчунавања.
Улога семантике:
програмер може да разуме како се програм извршава пре његовог покретања као и шта мора да обезбеди приликом креирања компилатора разумевање карактеристика програмског језика и њихове интеракције доказивање својстава одређеног програмског језика
Семантика може да се опише формално и неформално. На пример, формална семантика олакшава писање компилатора, боље разумевање тога шта програм ради као и доказивање на пример тога да следећа наредба:
if 1 = 1 then S1 else S2
има исти ефекат као само S1.
Преглед Област формалне семантике обухвата следеће теме: дефиниција семантичких модела веза између различитих семантичких модела веза између различитих приступа значењу веза имеђу израчунавања и основних математичких структура које стоје иза тога, на пример из области логике, теорије скупова, теорије модела, теорије категорија итд.
Уско је повезана и са другим областима рачунарства и информатике попут дизајна програмских језика, компилирања, интерпретирања, верификације програма.
Статичка семантика Статичка семантика дефинише ограничења на структуре валидних текстова које је тешко или немогуће изразити користећи стандардне синтатичке формализме. За језике који се компилирају, статичка семантика обухвата она семантичка правила која се могу проверити у току компилације. На пример, провера да ли је сваки идентификатор декларисан пре употребе (у оним програмским језицима који захтевају декларацију пре употребе) или да су ознаке у case наредби различите. Многа важна ограничења овог типа, попут провере тога да ли су идентификатори употребљени у исправном контексту (нпр. не додајемо цео број имену функције) или да позиви у подрутинама имају одговарајући број и тип аргумената, се могу остварити тако што ћемо их дефинисати као правила у логици која се зове систем типова.
Семантички модели Појмови попут семантичке мреже и семантичког дата модела се користе за описивање посебних типова дата модела које карактерише употреба директних графова у којима темена означавају концепте или ентитете у свету, а лукови означавају везе између њих. Семантички веб представља екстензију светске мреже која настаје уграђивањем семантичких метаподатака коришћењем техника семантичког дата моделовања попут RDF-a и OWL-а.
Подела Аксиоматска семантика Операциона семантика Денотациона семантика
Аксиоматска семантика
Аксиоматска семантика је једна врста приступа заснована на математичкој логици која служи за доказивање коректности рачунарског програма. Она дефинише значење команди у програму тако што описује њихов ефекат на наредбе везане за стање рачунарског програма. Значење рачунарског програма није експлицитнно дато, већ су својства језичких контруката дефинисана преко аксиома и правила инференције симболичке логике. Својство програма је изведено из њих да би се конструисао формалан доказ својства. Дакле, аксиоматска семантика нам не даје директно значење програма, већ оно што може бити доказано о програму. Постоје две врсте примене: верификација програма и спецификација семантике програма.
Кључна идеја је да се не дефинише понашање програма (као операционом или денотационом семантиком) и извоћење из тих дефиниција, већ се узимају сами закони тих дефиниција. Значење термина је оно што може бити доказано о њему. Лепота аксиоматских метода јесте што се фокусирају на процес закључивања, процес који је у рачунарству довео до великих идеја попут инваријанти.
Једноставни системи могу нпр. подржати доказе да је један програм еквивалентан другом, које год значење имали. Сложенији системи могу подржавати и доказе о улазно/излазним својствима програма. Аксиоматске дефиниције су апстрактније од денотационих и операционих, тако да својства доказана о програму можда не буду довољна да у потпуности одреде значење програма. Ова врста формата је најбоља за прелиминарне спецификације језика, као и за достављање документације о занимљивим својствима језика корисницима.
Тврдње Логичке изразе који се јављају у аксиоматској семантици зовемо предикати, односно тврдње. Они описују ограничења програмских променљивих. Постоје две врсте тврдњи: предуслов и постуслов. Аксиоматска семантика има за основу математичку логику, на пример Хорову логику. Хорова тројка {P} C {Q} описује како извршавање дела кода мења стање израчунавања; ако је испуњен предуслов {P}, извршавање команде C води до постуслова {Q}. Хорова логика обезбеђује аксиоме и правила извођења за све консртукте једноставног императивног програмског језика. Пример за постусловну тврдњу: sum = 2 * x + 1 {sum > 1}.
Једна од могућности за предусловну тврдњу везану за овај израз била би: {x > 10}.
Најслабији предуслов Најслабији предуслов је најмањи рестриктивни предуслов који ће гарантовати валидност повезаног постуслова. У претходном примеру {x > 10}, {x > 50} и {x > 1000} су све валидни предуслови, али {x > 0} је најслабији предуслов. Правило закључивања је метод да истинитост једне тврдње нађемо на основу истинитости других тврдњи. Општи облик правила изгледа овако:
Ово правило каже да ако су S1, S2,..., Sn истинити онда можемо закључити и о истинитости тврдње S. Горњи део правила се зове претходник, а доњи доследник.
Најслабији предуслов за секвенцу изјава не може се описати аксиомом, јер предуслов зависи од посебних изјава у секвенци. У том случају, предуслов се може описати само помоћу правила закључивања. Нека су S1 и S2 две упоредне програмске изјаве. Ако S1 и S2 имају следеће предуслове и постуслове: {P1} S1 {P2}, {P2} S2 {P3}, онда правило закључивања ове секције гласи:
Дакле, за овај пример, {P1} S1; S2 {P3} описује аксиоматску семантику секвенце S1; S2.
Правило извођења селекције чији је општи облик if B then S1 else S2 је:
Ово правило указује на то да изјава мора бити доказана и када је логичка вредност израза тачна и када је нетачна. Према правилу, треба нам предуслов P који може бити употребљен као предуслов и then и else клаузуле. Уколико B испуњава предуслов, онда ће се извршити then грана, а уколико не испуњава извршиће се else грана.
Још једна есенцијална конструкција императивних језика јесте while петља. Рачунање најслабијег предуслова за while петљу је знатно теже него за секвенце, зато што број итерација не може увек бити одређен. Проблем рачунања најслабијег предуслова за петље је сличан проблему доказивања теореме о природним бројевима. Први корак је пронаћи инваријанту петље, која је кључна за проналазак најслабијег предуслова. Правило закључивања гласи:
I је инваријанта петље. Иако делује лако, није ни мало тако. Комплексност лежи у проналаску одговарајуће инваријанте петље. Аксиоматски опис while петље гласи:
{P} while B do S end {Q}.
Евалуације За дефинисање семантике комплетног програмског језика користећи аксиоматски метод мора постојати аксиома или правило извођења за сваки тип изјаве у језику. Доказано је да је дефинисање аксиома и правила извођења за неке изјаве тежак задатак. Аксиоматска семантика је моћан алат за истраживање коректности програма и обезбеђује одличан оквир за разумевање програма, било током њихове конструкције или касније. Њена корисност у описивању значења програмских језика корисницима језика и писцима компајлера је, међутим, врло ограничена.
Операциона семантика
Операциона семантика је категорија формалне семантике програмских језика у којој одређена жељена својства програма, као што су тачност, сигурност и безбедност, су верификована изградњом доказа из логичких изјава о њиховом извршењу и процедурама, а не везивањем математичког значења са њеним условима (денотациона семантика). Операциона семантика је класификована у две категорије: структурна операциона семантика формално која описује како поједини кораци у израчунавању утичу на систем компјутера, док природна семантика описују како се добијају крајњи резултати извршења. Остали приступи формалној семантици програмских језика укључују аксиоматску семантику и денотациону семантику.
Операциона семантика програмских језика описује како се исправан програм тумачи као низ рачунарских корака. Овај низ корака представља значење програма. У функционалном програмирању, завршни корак у низу враћа вредност програма.(Генерално гледано, постоје многе вредности за појединачан програм, зато што програм може бити недетерминистички, чак и за детерминистички програм могу постојати многе рачунарске секвенце с обзиром да значења не морају одредити који тачно низ операција доводи до дате вредности.)
Концепт операционе семантике је коришћен први пут у дефинисању семантике Алгол 68. Следећа изјава је прерађени цитат иѕ АЛГОЛ 68 иѕвештаја:
Значење програма у строгом језику је објашњен преко хипотетичког рачунара који врши низ акција које чине израду тог програма. (Алгол68, Одељак 2)
Прва употреба термина операциона семантика у свом садашњем смислу се приписује Dana Scott-a. Оно што следи је цитат из Скотових папира о формалној семантици, у којој се помињу "операциони" аспекти семантике.
То је све веома добро да тежи више 'апстрактно' и на 'чистији' приступ семантици, али ако је у плану да буде добро у било ком смислу, операциони аспекти не могу се у потпуности игнорисати.
Можда је прво формално оличење оперативне семантике употреба ламбда рачуна за дефинисање семантике ЛИСП-а од стране Џона Макартија.'Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I'., Преузето 13.10.2006.. Приступи Gordon Plotkin је увео структурну операциону семантику, Robert Hieb и Matthias Felleisen контекст смањења, и Gilles Kahn природну семантику.
Структурна операциона семантика
Структурну операциону семантику је увео Gordon Plotkin као логичан начин да се дефинише операциона семантика. Основна идеја иза СОС је да дефинише понашање програма у погледу понашања његових делова, чиме се обезбеђује структурни, то јест, синтаксно оријентисан и индуктивни, поглед на оперативну семантику. СОС спецификација дефинише понашање програма у смислу транзиције односа. СОС спецификације су у форми низа правила која дефинишу валидне транзиције од делова синтаксе у смислу транзиције његових компоненти.
Таква дефиниција омогућава формалну анализу понашања програма, дозвољавајући проучавање односа између програма. Важни односи укључују симулације унапред и бисимулацију. Они су нарочито корисни у контексту теорије конкуренције.
Захваљујући својим интуитивним изгледима и структури која се лако прати, СОС је стекао велику популарност и постао стандард у пракси у дефинисању оперативне семантике. Као знак успеха, оригинални извештај (тзв Архус извештај) на СОС (Плоткин81) је привукао више од 1000 цитата у складу са CiteSeer.CiteSeer, што га чини једним од највећих наведених техничких извештаја у информатици.
Редукциона семантика
Редукциона семантика је алтернативан вид операционе семантике помоћу такозваних контекста смањење. Методу је увео Robert Hieb и Matthias Felleisen 1992. године као техника за формализовање опште теорије алгебре за управљање током и стањима. На пример, граматика позива по вредности ламбда рачуна и њени контексти могу бити задати као:
Контекст укључује празнину где се члан може укључити.
Облик контекста указује где у редукција може да се јави (т.ј., где се члан може укључити) члан.
Да опише семантику за дати језик, аксиоме или правила за смањење обезбеђују:
Ова једна аксиома је бета правило за ламбда рачун. Контексти за смањење показују како се ово правило користи са више сложених услова. Посебно, ово правило може да изазове за аргумент