Семантика на програмски јазик
Во теоријата на програмскиот јазик, семантиката е областа што се занимава со ригорозна математичка студија за значењето на програмските јазици . Тоа го прави со проценка на значењето на синтаксички валидни жици дефинирани со специфичен програмски јазик, покажувајќи ја вклучената пресметка. Во таков случај, проценката би била од синтетички невалидни жици, резултатот би бил не-пресметка. Семантиката ги опишува процесите што компјутер ги следи при извршување програма на тој специфичен јазик. Ова може да се покаже со опишување на врската помеѓу влезот и излезот на програмата или објаснување за тоа како програмата ќе се извршува на одредена платформа, со што се создава модел на пресметка .
На пример, формалната семантика помага да се напишат компајлери, подобро да се разбере што прави програмата и да се докаже, на пример, следново ако е изјава
ако 1 == 1, тогаш S1 друго S2
има ист ефект како што S1 на само.
Преглед
[уреди | уреди извор]Областа на формална семантика ги опфаќа сите следниве:
- Дефиницијата на семантичките модели
- Односите помеѓу различни семантички модели
- Односите помеѓу различните пристапи кон значењето
- Односот помеѓу пресметувањето и основните математички структури од области како што се логика, теорија на множества, теорија на модели, теорија на категории и сл.
Има блиски врски со други области на компјутерски науки како што се дизајн на јазик за програмирање, теорија на типови, компајлери и толкувачи, верификација на програмата и проверка на модели .
Пристапи
[уреди | уреди извор]Постојат многу пристапи кон формалната семантика; овие припаѓаат на три главни класи:
- Дентационална семантика, при што секоја фраза на јазикот се толкува како ознака, т.е. концептуално значење за кое може да се мисли апстрактно. Ваквите означувања честопати се математички предмети што живеат во математички простор, но не е услов тие да бидат така. Како практична потреба, означувањата се опишани со употреба на некоја форма на математичка нотација, која пак може да се формализира како означувачки металозик. На пример, дентациската семантика на функционалните јазици честопати го преведува јазикот во теорија на домени . Денационалните семантички описи можат да послужат и како композициски преводи од програмски јазик во ознаката на металозик и да се користат како основа за дизајнирање на компајлери .
- Оперативна семантика, при што извршувањето на јазикот се опишува директно (отколку со превод). Оперативната семантика лабаво одговара на толкувањето, иако повторно „јазикот на спроведување“ на толкувачот е генерално математички формализам. Оперативната семантика може да дефинира апстрактна машина (како што е машината SECD ) и да им дава значење на фразите со опишување на транзициите што ги предизвикуваат во состојбите на машината. Алтернативно, како и со чистиот пресметковен ламбда, оперативната семантика може да се дефинира преку синтаксички трансформации на фразите на самиот јазик;
- Аксиоматска семантика, при што се дава значење на фразите со опишување на аксиомите што важат за нив. Аксиоматската семантика не прави разлика помеѓу значењето на фразата и логичките формули што ја опишуваат; неговото значење е токму она што може да се докаже за тоа во некоја логика. Канонскиот пример за аксиоматска семантика е хоареовата логика.
Разликите помеѓу трите широки класи на пристапи понекогаш можат да бидат нејасни, но сите познати пристапи кон формалната семантика ги користат горенаведените техники или нивна комбинација.
Освен изборот помеѓу ознаките, оперативните или аксиоматските пристапи, повеќето варијации во формалните семантички системи произлегуваат од изборот на поддршка на математички формализам.
Варијации
[уреди | уреди извор]Некои варијации на формалната семантика го вклучуваат следново:
- Дејствената семантика е пристап кој се обидува да ја модулира денотациската семантика, поделејќи го процесот на формализација во два слоја (макро и микросемантика) и предодредување на три семантички ентитети (акции, податоци и приноси) за поедноставување на спецификацијата;
- Алгебарската семантика е форма на аксиоматска семантика заснована на алгебарски закони за опишување и расудување за програмската семантика на формален начин;
- Граматиките на атрибути дефинираат системи што систематски пресметуваат „ метаподатоци “ (наречени атрибути ) за различните случаи на синтаксата на јазикот . Граматиките на атрибути можат да се разберат како дентациска семантика каде целниот јазик е едноставно оригиналниот јазик збогатен со прибелешки за атрибути. Покрај формалната семантика, граматиките на атрибути се користат и за генерирање на код во компајлерите и за зголемување на редовни или контекстни граматики со контекст чувствителни услови;
- Категорична (или „функторијална“) семантика ја користи теоријата на категоријата како основен математички формализам. Категоричката семантика обично се докажува дека одговара на некои аксиоматски семантики што дава синтаксичка презентација на категоричните структури. Исто така, дентациската семантика е често примери на општа категорична семантика;
- Семантиката на истовременост е целосен термин за која било формална семантика што опишува истовремени пресметки. Историски важни истовремени формализми вклучуваат модел на глумец и пресметковни процеси ;
- Семантиката на игри користи метафора инспирирана од теоријата на игри .
- Предактичката семантика на трансформаторот, развиена од Едсгер В. Дијкстра, го опишува значењето на фрагмент од програмата како функција што ја трансформира постусловата кон предусловот потребен за негово воспоставување.
Опишување на односите
[уреди | уреди извор]Од различни причини, можеби ќе посакаме да се опишат односите помеѓу различна формална семантика. На пример:
- Да докаже дека одредена оперативна семантика за еден јазик ги задоволува логичките формули на аксиоматската семантика за тој јазик. Таквиот доказ покажува дека е „здраво“ да се размислува за одредена (оперативна) стратегија за толкување со користење на одреден (аксиоматски) доказ систем .
- Да се докаже дека оперативната семантика над машина со високо ниво е поврзана со симулација со семантиката преку машина со ниско ниво, при што апстрактната машина со ниско ниво содржи повеќе примитивни операции од дефинирањето на даден јазик со висока апстрактна машина. Таквиот доказ покажува дека машината со ниско ниво „верно ја спроведува“ машината на високо ниво.
Исто така, можно е да се поврзат повеќе семантики преку апстракции преку теоријата на апстрактно толкување .
Историја
[уреди | уреди извор]Роберт В. Флојд бил заслужен за основање на полето на програмирање на јазична семантика во Флојд (1967).[1]
Наводи
[уреди | уреди извор]- ↑ Knuth, Donald E. „Memorial Resolution: Robert W. Floyd (1936–2001)“ (PDF). Stanford University Faculty Memorials. Stanford Historical Society.
Дополнителна литература
[уреди | уреди извор]- Учебници
- Флојд, Роберт В. (1967). „Assigning Meanings to Programs“ (PDF). Во Schwartz, J.T. (уред.). Mathematical Aspects of Computer Science. Proceedings of Symposium on Applied Mathematics. 19. American Mathematical Society. стр. 19–32. ISBN 0821867288.
- Хенеси, М. (1990). The semantics of programming languages: an elementary introduction using structural operational semantics. Wiley. ISBN 978-0-471-92772-3.
- Тенент, Роберт Д. (1991). Semantics of Programming Languages. Prentice Hall. ISBN 978-0-13-805599-8.
- Гунтер, Карл (1992). Semantics of Programming Languages. MIT Press. ISBN 0-262-07143-6.
- Нилсон, Х. Р.; Нилсон, Флеминг (1992). Semantics With Applications: A Formal Introduction (PDF). Wiley. ISBN 978-0-471-92980-2. Архивирано од изворникот (PDF) на 2012-04-17. Посетено на 2020-02-22.
- Винксел, Глин (1993). The Formal Semantics of Programming Languages: An Introduction. MIT Press. ISBN 0-262-73103-7.
- Мичел, Џон К. (1995). Foundations for Programming Languages (Postscript).
- Слонегер, Кенет; Курц, Бери Л. (1995). Formal Syntax and Semantics of Programming Languages. Addison-Wesley. ISBN 0-201-65697-3.
- Рејнолдс, Џон К. (1998). Theories of Programming Languages. Cambridge University Press. ISBN 0-521-59414-6.
- Харпер, Роберт (2006). Practical Foundations for Programming Languages (PDF). Архивирано од изворникот (PDF) на 2007-06-27. (Working draft)
- Нилсон, Х. Р.; Нилсон, Флеминг (2007). Semantics with Applications: An Appetizer. Springer. ISBN 978-1-84628-692-6.
- Стамп, Арон (2014). Programming Language Foundations. Wiley. ISBN 978-1-118-00747-1.
- Кришнамурти, Ширам (2012). „Programming Languages: Application and Interpretation“ (2. изд.).
- Белешки од предавања
- Винскел, Глин. „Denotational Semantics“ (PDF). University of Cambridge.
Надворешни врски
[уреди | уреди извор]- Аби, Ентони (2004). Introduction to Programming Languages. Архивирано од изворникот на 19 јуни 2015. Semantics.