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

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

На пример, формалната семантика помага да се напишат компајлери, подобро да се разбере што прави програмата и да се докаже, на пример, следново ако е изјава

 ако 1 == 1, тогаш S1 друго S2 

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

Преглед

Областа на формална семантика ги опфаќа сите следниве:

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

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

Пристапи

Постојат многу пристапи кон формалната семантика; овие припаѓаат на три главни класи:

• Дентационална семантика, при што секоја фраза на јазикот се толкува како ознака, т.е. концептуално значење за кое може да се мисли апстрактно. Ваквите означувања честопати се математички предмети што живеат во математички простор, но не е услов тие да бидат така. Како практична потреба, означувањата се опишани со употреба на некоја форма на математичка нотација, која пак може да се формализира како означувачки металозик. На пример, дентациската семантика на функционалните јазици честопати го преведува јазикот во теорија на домени . Денационалните семантички описи можат да послужат и како композициски преводи од програмски јазик во ознаката на металозик и да се користат како основа за дизајнирање на компајлери .
• Оперативна семантика, при што извршувањето на јазикот се опишува директно (отколку со превод). Оперативната семантика лабаво одговара на толкувањето, иако повторно „јазикот на спроведување“ на толкувачот е генерално математички формализам. Оперативната семантика може да дефинира апстрактна машина (како што е машината SECD ) и да им дава значење на фразите со опишување на транзициите што ги предизвикуваат во состојбите на машината. Алтернативно, како и со чистиот пресметковен ламбда, оперативната семантика може да се дефинира преку синтаксички трансформации на фразите на самиот јазик;
• Аксиоматска семантика, при што се дава значење на фразите со опишување на аксиомите што важат за нив. Аксиоматската семантика не прави разлика помеѓу значењето на фразата и логичките формули што ја опишуваат; неговото значење е токму она што може да се докаже за тоа во некоја логика. Канонскиот пример за аксиоматска семантика е хоареовата логика.

Разликите помеѓу трите широки класи на пристапи понекогаш можат да бидат нејасни, но сите познати пристапи кон формалната семантика ги користат горенаведените техники или нивна комбинација.

Освен изборот помеѓу ознаките, оперативните или аксиоматските пристапи, повеќето варијации во формалните семантички системи произлегуваат од изборот на поддршка на математички формализам.

Варијации

Некои варијации на формалната семантика го вклучуваат следново:

• Дејствената семантика е пристап кој се обидува да ја модулира денотациската семантика, поделејќи го процесот на формализација во два слоја (макро и микросемантика) и предодредување на три семантички ентитети (акции, податоци и приноси) за поедноставување на спецификацијата;
• Алгебарската семантика е форма на аксиоматска семантика заснована на алгебарски закони за опишување и расудување за програмската семантика на формален начин;
• Граматиките на атрибути дефинираат системи што систематски пресметуваат „ метаподатоци “ (наречени атрибути ) за различните случаи на синтаксата на јазикот . Граматиките на атрибути можат да се разберат како дентациска семантика каде целниот јазик е едноставно оригиналниот јазик збогатен со прибелешки за атрибути. Покрај формалната семантика, граматиките на атрибути се користат и за генерирање на код во компајлерите и за зголемување на редовни или контекстни граматики со контекст чувствителни услови;
• Категорична (или „функторијална“) семантика ја користи теоријата на категоријата како основен математички формализам. Категоричката семантика обично се докажува дека одговара на некои аксиоматски семантики што дава синтаксичка презентација на категоричните структури. Исто така, дентациската семантика е често примери на општа категорична семантика;
• Семантиката на истовременост е целосен термин за која било формална семантика што опишува истовремени пресметки. Историски важни истовремени формализми вклучуваат модел на глумец и пресметковни процеси ;
• Семантиката на игри користи метафора инспирирана од теоријата на игри .
• Предактичката семантика на трансформаторот, развиена од Едсгер В. Дијкстра, го опишува значењето на фрагмент од програмата како функција што ја трансформира постусловата кон предусловот потребен за негово воспоставување.

Опишување на односите

Од различни причини, можеби ќе посакаме да се опишат односите помеѓу различна формална семантика. На пример:

• Да докаже дека одредена оперативна семантика за еден јазик ги задоволува логичките формули на аксиоматската семантика за тој јазик. Таквиот доказ покажува дека е „здраво“ да се размислува за одредена (оперативна) стратегија за толкување со користење на одреден (аксиоматски) доказ систем .
• Да се докаже дека оперативната семантика над машина со високо ниво е поврзана со симулација со семантиката преку машина со ниско ниво, при што апстрактната машина со ниско ниво содржи повеќе примитивни операции од дефинирањето на даден јазик со висока апстрактна машина. Таквиот доказ покажува дека машината со ниско ниво „верно ја спроведува“ машината на високо ниво.

Исто така, можно е да се поврзат повеќе семантики преку апстракции преку теоријата на апстрактно толкување .

Историја

Роберт В. Флојд бил заслужен за основање на полето на програмирање на јазична семантика во Флојд (1967).

Дополнителна литература

Учебници