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

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

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

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

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

    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} је најслабији предуслов. Правило закључивања је метод да истинитост једне тврдње нађемо на основу истинитости других тврдњи. Општи облик правила изгледа овако:

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

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

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

    ${\frac {\{P1\}S1\{P2\},\{P2\}S2\{P3\}}{\{P1\}S1,S2\{P3\}}}$

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

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

    ${\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 петљу је знатно теже него за секвенце, зато што број итерација не може увек бити одређен. Проблем рачунања најслабијег предуслова за петље је сличан проблему доказивања теореме о природним бројевима. Први корак је пронаћи инваријанту петље, која је кључна за проналазак најслабијег предуслова. Правило закључивања гласи:

    ${\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}.

Евалуације

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

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

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

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

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

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

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

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

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

Приступи

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

Структурна операциона семантика

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

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

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

Редукциона семантика

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

$e=v\;|\;(e\;e)\;|\;x\quad \quad v=\lambda x.e\quad \quad C=\left[\,\right]\;|\;(C\;e)\;|\;(v\;C)$

Контекст $C$ укључује празнину $\left[\,\right]$ где се члан може укључити.

Облик контекста указује где у редукција може да се јави (т.ј., где се члан може укључити) члан.

Да опише семантику за дати језик, аксиоме или правила за смањење обезбеђују:

$(\lambda x.e\;v)\longrightarrow e\,\left[x/v\right]\quad (\mathrm {\beta } )$

Ова једна аксиома је бета правило за ламбда рачун. Контексти за смањење показују како се ово правило користи са више сложених услова. Посебно, ово правило може да изазове за аргумент апликације нешто као $((\lambda x.x\;\lambda x.x)\lambda x.(x\;x))$ јер постоји контекст $([\,]\;\lambda x.(x\;x))$ који одговара датом члану. У том случају, контексти јединствено разлажу услове тако да је само једна редукција могућа у било ком датом кораку. Проширујући аксиому да одговара контекстима смањења даје компатибилно затварање. Узимајући рефлексивно, транзитивно затварање овог односа даје однос смањења за тај језик.

Техника је корисна за лакоћу у којој контексти смањење моделирају стања или контролне конструкте . Поред тога, семантика смањења се користи као модел објектно-оријентисаних језика, уговорних система и других функција језика.

Природна семантика

Природна семантика такође позната и као, релациона смеантика и евалуциона семантика. Ова семантика је уведена под називом природни семантика од стране Gilles Kahn-а приликом представљања Mini-ML, чистог дијалекта ML језика.

Неки могу сматрати природну семантику као дефиницију функције, или уопште односа, тумачење сваког језичког конструктора у одговарајућој области. Њена интуитивност је популаран избор за семантику спецификације у програмским језицима, али има неке недостатке који је чине незгодном или је немогуће њено коришћење у многим ситуацијама, као што су језици са интензивним-контролним карактеристика или конкурентни.

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

Поређење

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

Природна семантика има предност јер је често једноставнија (потребно мање правила за закључивање) и често директно одговара ефикасној имплементацији преводиоца језика. Може да доведе до једноставнијих доказа, на пример, када се доказује очување исправности неке програмске трансформације.

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

Денотациона семантика

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

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

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

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

Историјски развој

Денотациона семантика је развијена 1960-их на Оxфорду у истраживачкој групи под вођством Christopher Strachey. Dana Scott је методи дао математичку строгоћу, а у комбинацији са нотацијском елеганцијом Strachey-а је с временом еволуирала из средства анализе у алат дизајна и имплементације програмских језика.

Денотациона семантика је развијена за модерне програмске језике који користе особине као што су конкурентност и изузеци, итд., Concurrent ML, CSP, and Haskell. Семантика ових језика је композиција у којој денотација дела програма зависи од денотације неког његовог дела. На пример, значење апликативног израза f(E1,E2) је дефинисана у терминима семантике својих подпрограма f, Е1, Е2. У модерном програмском језику , Е1 и Е2 могу се паралелно израчунати и извршање једног може имати утицаја на израчунавање другог тако што и Е1 и Е2 имају заједничке објекте доводећи до тога да њихове денотације морају бити дефинисане са међусобном зависношћу. Такође, Е1 и Е2 могу избацивати изузетак који би могао да заврши извршавање другог. У наставку ће бити описани специјални случајеви семантика ових програмских језика.

Денотација рекурзивних програма

Na primer, део кода n*m чини денотацију која повезује две слободне промењиве n и m. Ако промењива n има вредност 3 и m има вредност 5, онда денотација има вредност 15.

Функција може бити задата као скуп уређених парова, где је сваки пар сачињен од два дела (1) је аргумент функције и (2) вредност функције позване за тај аргумент. На пример, скуп уређених парова {[0 1] [4 3]} је денотација функције са вредношћу 1 кад је аргумент функције 0, и вредност 3 за аргумент 4, иначе није дефиисана.

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

    ::factorial ≡  λ(n) if (n==0) then 1 else n*factorial(n-1).

Решење је да се изгради дентација апроксимацијом почевши од празног скупа уређених парова, и овај скуп записујемо са {}. Ако је {} укључено у горенаведену дефиницију факторијела онда је денотација {[0 1]}, што је боља апроксимација од факторијела. Итерирамо: Ако је {[0 1]} укључено у дефиницију онда је денотација {[0 1] [1 1]}. Сада на апроксимацију factorial-а моѕемо да гледамо кад улаз за F на следећи начин:

    ::λ(F) λ(n) if (n==0) then 1 else n*F(n-1).

У наставку је представљен ланац итерација где Fⁱ указује на i-итерација F

• F⁰({}) је функција која нигде није дефинисана {}
• F¹({}) је функција {[0 1]} која је дефинисана у 0 да буде 1, и није дефинисана више нигде;
• F⁵({}) је функција {[0 1] [1 1] [2 2] [3 6] [4 24]}

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

    ::$\bigsqcup _{i\in \mathbb {N} }F^{i}(\{\}).$

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

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

Принцип композиције

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

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

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

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

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

Литература

• R. Sebesta: "Concepts of programming languages", Addison Wesley, (10. ed.), 2012.
• Милена Вујошевић Јаничић, Дизајн програмских језика

Види још

• Програмирање
• Програмски језик