stringtranslate.com

Семантика (информатика)

В теории языков программирования семантика это строгое математическое изучение смысла языков программирования . [1] Семантика присваивает вычислительное значение допустимым строкам в синтаксисе языка программирования . Она тесно связана с семантикой математических доказательств и часто пересекается с ней .

Семантика описывает процессы, которым следует компьютер при выполнении программы на этом конкретном языке. Это можно сделать, описав связь между входом и выходом программы или дав объяснение того, как программа будет выполняться на определенной платформе , тем самым создавая модель вычислений .

История

В 1967 году Роберт В. Флойд опубликовал статью «Присвоение значений программам »; его главной целью было «создание строгого стандарта для доказательств компьютерных программ, включая доказательства корректности , эквивалентности и завершения». [2] [3] Флойд далее писал: [2]

Семантическое определение языка программирования, в нашем подходе, основано на синтаксическом определении. Оно должно указывать, какие из фраз в синтаксически правильной программе представляют команды , и какие условия должны быть наложены на интерпретацию в окрестности каждой команды.

В 1969 году Тони Хоар опубликовал статью о логике Хоара, основанную на идеях Флойда, которые теперь иногда называют аксиоматической семантикой . [4] [5]

В 1970-х годах появились термины «операциональная семантика» и «денотационная семантика» . [5]

Обзор

Область формальной семантики охватывает все следующее:

Она тесно связана с другими областями компьютерной науки, такими как проектирование языков программирования , теория типов , компиляторы и интерпретаторы , верификация программ и проверка моделей .

Подходы

Существует множество подходов к формальной семантике; они относятся к трем основным классам:

Помимо выбора между денотационным, операциональным или аксиоматическим подходами, большинство вариаций формальных семантических систем возникают из выбора поддерживающего математического формализма. [ необходима ссылка ]

Вариации

Некоторые варианты формальной семантики включают следующее:

Описание отношений

По разным причинам может возникнуть желание описать отношения между различными формальными семантиками. Например:

Также возможно связать множественные семантики посредством абстракций посредством теории абстрактной интерпретации . [ необходима ссылка ]

Смотрите также

Ссылки

  1. ^ Goguen, Joseph A. (1975). "Семантика вычислений". Теория категорий в применении к вычислениям и управлению . Lecture Notes in Computer Science. Vol. 25. Springer . pp. 151–163. doi :10.1007/3-540-07142-3_75. ISBN 978-3-540-07142-6.
  2. ^ ab Floyd, Robert W. (1967). "Присвоение значений программам" (PDF) . В Schwartz, JT (ред.). Математические аспекты компьютерной науки. Труды симпозиума по прикладной математике. Том 19. Американское математическое общество. стр. 19–32. ISBN 0821867288.
  3. ^ Кнут, Дональд Э. «Памятная резолюция: Роберт У. Флойд (1936–2001)» (PDF) . Мемориалы факультета Стэнфордского университета . Историческое общество Стэнфорда.
  4. ^ Hoare, CAR (октябрь 1969). «Аксиоматическая основа компьютерного программирования». Communications of the ACM . 12 (10): 576–580. doi : 10.1145/363235.363259 . S2CID  207726175.
  5. ^ ab Winskel, Glynn (1993). Формальная семантика языков программирования: введение. Кембридж, Массачусетс: MIT Press. стр. xv. ISBN 978-0-262-23169-5.
  6. ^ Шмидт, Дэвид А. (1986). Денотационная семантика: методология развития языка . William C. Brown Publishers. ISBN 9780205104505.
  7. ^ Плоткин, Гордон Д. (1981). Структурный подход к операционной семантике (Отчет). Технический отчет DAIMI FN-19. Кафедра компьютерных наук, Орхусский университет .
  8. ^ ab Goguen, Joseph A. ; Thatcher, James W.; Wagner, Eric G.; Wright, Jesse B. (1977). «Начальная семантика алгебры и непрерывные алгебры». Journal of the ACM . 24 (1): 68–95. doi : 10.1145/321992.321997 . S2CID  11060837.
  9. ^ Мосс, Питер Д. (1996). Теория и практика семантики действий (Отчет). Отчет BRICS RS9653. Орхусский университет .
  10. ^ Дерансарт, Пьер; Журдан, Мартен; Лорхо, Бернар (1988). «Атрибутивные грамматики: определения, системы и библиография» . Конспект лекций по информатике 323. Springer-Verlag . ISBN 9780387500560.
  11. ^ Ловер, Ф. Уильям (1963). «Функториальная семантика алгебраических теорий». Труды Национальной академии наук Соединенных Штатов Америки . 50 (5): 869–872. Bibcode :1963PNAS...50..869L. doi : 10.1073/pnas.50.5.869 . PMC 221940 . PMID  16591125. 
  12. ^ Анджей Тарлецкий; Род М. Берстолл ; Джозеф А. Гоген (1991). «Некоторые фундаментальные алгебраические инструменты для семантики вычислений: Часть 3. Индексированные категории». Теоретическая информатика . 91 (2): 239–264. doi : 10.1016/0304-3975(91)90085-G .
  13. ^ Бэтти, Марк; Мемариан, Кайван; Ниенхейс, Киндилан; Пишон-Фарабо, Джин; Сьюэлл, Питер (2015). «Проблема семантики параллелизма языков программирования» (PDF) . Труды Европейского симпозиума по языкам и системам программирования . Springer . стр. 283–307. doi : 10.1007/978-3-662-46669-8_12 .
  14. ^ Абрамски, Сэмсон (2009). «Семантика взаимодействия: введение в игровую семантику». В Andrew M. Pitts; P. Dybjer (ред.). Семантика и логика вычислений. Cambridge University Press. стр. 1–32. doi :10.1017/CBO9780511526619.002. ISBN 9780521580571.
  15. ^ Дейкстра, Эдсгер В. (1975). «Защищенные команды, неопределенность и формальный вывод программ». Сообщения ACM . 18 (8): 453–457. doi : 10.1145/360933.360975 . S2CID  1679242.

Дальнейшее чтение

Учебники
Конспект лекций

Внешние ссылки