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

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

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

История

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

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

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

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

Обзор

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

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

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

Подходы

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

Денотационная семантика [^6] , посредством которой каждая фраза в языке интерпретируется как денотация , т.е. концептуальное значение, которое можно мыслить абстрактно. Такие денотации часто являются математическими объектами, населяющими математическое пространство, но это не обязательно, чтобы они были таковыми. В качестве практической необходимости денотации описываются с использованием некоторой формы математической нотации, которая, в свою очередь, может быть формализована как денотационный метаязык. Например, денотационная семантика функциональных языков часто переводит язык в теорию предметной области . Денотационные семантические описания также могут служить композиционными переводами с языка программирования на денотационный метаязык и использоваться в качестве основы для проектирования компиляторов .
Операционная семантика ,^[7] посредством которой выполнение языка описывается напрямую (а не переводом). Операционная семантика примерно соответствует интерпретации , хотя опять же «язык реализации» интерпретатора обычно является математическим формализмом. Операционная семантика может определять абстрактную машину (такую как машина SECD ) и придавать смысл фразам, описывая переходы, которые они вызывают в состояниях машины. В качестве альтернативы, как и в случае с чистым лямбда-исчислением , операционная семантика может быть определена через синтаксические преобразования фраз самого языка;
Аксиоматическая семантика ,^[8] посредством которой фразам придается значение путем описания аксиом , которые к ним применяются. Аксиоматическая семантика не делает различий между значением фразы и логическими формулами, которые ее описывают; ее значение — это именно то, что может быть доказано о ней в некоторой логике. Каноническим примером аксиоматической семантики является логика Хоара .

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

Вариации

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

Семантика действий^[9] — это подход, который пытается модуляризировать денотационную семантику, разделяя процесс формализации на два уровня (макро- и микросемантика) и предопределяя три семантические сущности (действия, данные и выходы) для упрощения спецификации;
Алгебраическая семантика^[8] — это форма аксиоматической семантики, основанная на алгебраических законах для описания и рассуждения о семантике программ формальным образом . Она также поддерживает денотационную семантику и операционную семантику ;
Атрибутивные грамматики^[10] определяют системы, которые систематически вычисляют « метаданные » (называемые атрибутами ) для различных случаев синтаксиса языка . Атрибутивные грамматики можно понимать как денотатную семантику, где целевой язык — это просто исходный язык, обогащенный атрибутными аннотациями. Помимо формальной семантики, атрибутивные грамматики также использовались для генерации кода в компиляторах и для дополнения регулярных или контекстно-свободных грамматик контекстно -зависимыми условиями;
Категориальная (или «функториальная») семантика ^[11] использует теорию категорий в качестве основного математического формализма. Категориальная семантика обычно доказывается соответствующей некоторой аксиоматической семантике, которая дает синтаксическое представление категориальных структур. Кроме того, денотационная семантика часто является примерами общей категориальной семантики;^[12]
Семантика параллелизма^[13] — это всеобъемлющий термин для любой формальной семантики, описывающей параллельные вычисления. Исторически важные параллельные формализмы включали модель актора и исчисления процесса ;
Игровая семантика^[14] использует метафору, вдохновленную теорией игр ;
Семантика преобразователя предикатов^[15] ,разработанная Эдсгером В. Дейкстрой , описывает значение фрагмента программы как функцию, преобразующую постусловие в предусловие, необходимое для его установления.

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

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

Доказать, что конкретная операциональная семантика для языка удовлетворяет логическим формулам аксиоматической семантики для этого языка. Такое доказательство демонстрирует, что «правильно» рассуждать о конкретной (операциональной) стратегии интерпретации, используя конкретную (аксиоматическую) систему доказательств .
Доказать, что операционная семантика на высокоуровневой машине связана симуляцией с семантикой на низкоуровневой машине, при этом низкоуровневая абстрактная машина содержит больше примитивных операций, чем определение высокоуровневой абстрактной машины данного языка. Такое доказательство демонстрирует, что низкоуровневая машина «добросовестно реализует» высокоуровневую машину.

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

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

Ссылки

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

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

Учебники

Флойд, Роберт В. (1967). «Присвоение значений программам» (PDF) . В Шварце, Дж. Т. (ред.). Математические аспекты компьютерной науки. Труды симпозиума по прикладной математике. Том 19. Американское математическое общество. С. 19–32. ISBN 0821867288.
Хеннесси, М. (1990). Семантика языков программирования: элементарное введение с использованием структурной операционной семантики . Wiley. ISBN 978-0-471-92772-3.
Теннент, Роберт Д. (1991). Семантика языков программирования. Prentice Hall. ISBN 978-0-13-805599-8.
Гюнтер, Карл (1992). Семантика языков программирования . MIT Press. ISBN 0-262-07143-6.
Нильсон, ХР; Нильсон, Флемминг (1992). Семантика с приложениями: формальное введение (PDF) . Wiley. ISBN 978-0-471-92980-2. Архивировано из оригинала (PDF) 2012-04-17 . Получено 2011-05-27 .
Уинскел, Глинн (1993). Формальная семантика языков программирования: Введение . MIT Press. ISBN 0-262-73103-7.
Митчелл, Джон К. (1995). Основы языков программирования (Постскриптум) .
Slonneger, Kenneth; Kurtz, Barry L. (1995). Формальный синтаксис и семантика языков программирования. Addison-Wesley. ISBN 0-201-65697-3.
Рейнольдс, Джон К. (1998). Теории языков программирования . Cambridge University Press. ISBN 0-521-59414-6.
Харпер, Роберт (2006). Практические основы языков программирования (PDF) . Архивировано из оригинала (PDF) 2007-06-27.(Рабочий проект)
Нильсон, Х.Р.; Нильсон, Флемминг (2007). Семантика с приложениями: закуска. Springer. ISBN 978-1-84628-692-6.
Стамп, Аарон (2014). Основы языка программирования . Wiley. ISBN 978-1-118-00747-1.
Кришнамурти, Шрирам (2012). «Языки программирования: применение и интерпретация» (2-е изд.).

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

Уинскел, Глинн. «Денотационная семантика» (PDF) . Кембриджский университет.

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

Aaby, Anthony (2004). Введение в языки программирования. Архивировано из оригинала 2015-06-19.Семантика.