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

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

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

История [ править ]

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

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

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

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

Обзор [ править ]

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

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

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

Подходы [ править ]

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

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

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

Вариации [ править ]

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

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

Описание отношений [ править ]

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

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

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

См. также [ править ]

Ссылки [ править ]

^ Гоген, Джозеф А. (1975). «Семантика вычислений». Теория категорий в применении к вычислениям и управлению . Конспекты лекций по информатике. Том. 25. Спрингер . стр. 151–163. дои : 10.1007/3-540-07142-3_75 . ISBN 978-3-540-07142-6 .
^ Jump up to: Перейти обратно: ^а ^б Флойд, Роберт В. (1967). «Придание значения программам» (PDF) . В Шварце, Дж. Т. (ред.). Математические аспекты информатики . Материалы симпозиума по прикладной математике. Том. 19. Американское математическое общество. стр. 19–32. ISBN 0821867288 .
^ Кнут, Дональд Э. «Мемориальная резолюция: Роберт В. Флойд (1936–2001)» (PDF) . Мемориалы факультетов Стэнфордского университета . Стэнфордское историческое общество.
^ Хоар, ЦАР (октябрь 1969 г.). «Аксиоматические основы компьютерного программирования» . Коммуникации АКМ . 12 (10): 576–580. дои : 10.1145/363235.363259 . S2CID 207726175 .
^ Jump up to: Перейти обратно: ^а ^б Винскель, Глинн (1993). Формальная семантика языков программирования: введение . Кембридж, Массачусетс: MIT Press. п. хв . ISBN 978-0-262-23169-5 .
^ Шмидт, Дэвид А. (1986). Денотационная семантика: методология развития языка . Издательство Уильяма К. Брауна. ISBN 9780205104505 .
^ Плоткин, Гордон Д. (1981). Структурный подход к операционной семантике (Отчет). Технический отчет DAIMI FN-19. Кафедра компьютерных наук Орхусского университета .
^ Jump up to: Перейти обратно: ^а ^б Гоген, Джозеф А .; Тэтчер, Джеймс В.; Вагнер, Эрик Г.; Райт, Джесси Б. (1977). «Семантика исходной алгебры и непрерывные алгебры» . Журнал АКМ . 24 (1): 68–95. дои : 10.1145/321992.321997 . S2CID 11060837 .
^ Моссес, Питер Д. (1996). Теория и практика семантики действия (Доклад). Отчет БРИКС RS9653. Орхусский университет .
^ Дерансар, Пьер; Журдан, Мартен; Лорхо, Бернар (1988). «Грамматики атрибутов: определения, системы и библиография . Конспекты лекций по информатике 323. Springer-Verlag . ISBN». 9780387500560 .
^ Ловер, Ф. Уильям (1963). «Функториальная семантика алгебраических теорий» . Труды Национальной академии наук Соединенных Штатов Америки . 50 (5): 869–872. Бибкод : 1963PNAS...50..869L . дои : 10.1073/pnas.50.5.869 . ПМК 221940 . ПМИД 16591125 .
^ Анджей Тарлецкий; Род М. Берстолл ; Джозеф А. Гоген (1991). «Некоторые фундаментальные алгебраические инструменты для семантики вычислений: Часть 3. Индексированные категории» . Теоретическая информатика . 91 (2): 239–264. дои : 10.1016/0304-3975(91)90085-G .
^ Бэтти, Марк; Мемариан, Кайван; Ниенхейс, Киндилан; Пишон-Фарабод, Жан; Сьюэлл, Питер (2015). «Проблема семантики параллелизма языка программирования» (PDF) . Труды Европейского симпозиума по языкам и системам программирования . Спрингер . стр. 283–307. дои : 10.1007/978-3-662-46669-8_12 .
^ Абрамский, Самсон (2009). «Семантика взаимодействия: введение в семантику игры». У Эндрю М. Питтса; П. Дюбьер (ред.). Семантика и логика вычислений . Издательство Кембриджского университета. стр. 1–32. дои : 10.1017/CBO9780511526619.002 . ISBN 9780521580571 .
^ Дейкстра, Эдсгер В. (1975). «Защищенные команды, неопределенность и формальный вывод программ» . Коммуникации АКМ . 18 (8): 453–457. дои : 10.1145/360933.360975 . S2CID 1679242 .

Дальнейшее чтение [ править ]

Учебники

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

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

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

Внешние ссылки [ править ]

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

[1] Гоген, Джозеф А. (1975). «Семантика вычислений». Теория категорий в применении к вычислениям и управлению . Конспекты лекций по информатике. Том. 25. Спрингер . стр. 151–163. дои : 10.1007/3-540-07142-3_75 . ISBN 978-3-540-07142-6 .

[floyd-2] Jump up to: Перейти обратно: ^а ^б Флойд, Роберт В. (1967). «Придание значения программам» (PDF) . В Шварце, Дж. Т. (ред.). Математические аспекты информатики . Материалы симпозиума по прикладной математике. Том. 19. Американское математическое общество. стр. 19–32. ISBN 0821867288 .

[3] Кнут, Дональд Э. «Мемориальная резолюция: Роберт В. Флойд (1936–2001)» (PDF) . Мемориалы факультетов Стэнфордского университета . Стэнфордское историческое общество.

[hoare-4] Хоар, ЦАР (октябрь 1969 г.). «Аксиоматические основы компьютерного программирования» . Коммуникации АКМ . 12 (10): 576–580. дои : 10.1145/363235.363259 . S2CID 207726175 .

[winskel-5] Jump up to: Перейти обратно: ^а ^б Винскель, Глинн (1993). Формальная семантика языков программирования: введение . Кембридж, Массачусетс: MIT Press. п. хв . ISBN 978-0-262-23169-5 .

[Schmidt1986-6] Шмидт, Дэвид А. (1986). Денотационная семантика: методология развития языка . Издательство Уильяма К. Брауна. ISBN 9780205104505 .

[Plotkin1981-7] Плоткин, Гордон Д. (1981). Структурный подход к операционной семантике (Отчет). Технический отчет DAIMI FN-19. Кафедра компьютерных наук Орхусского университета .

[Goguen77-8] Jump up to: Перейти обратно: ^а ^б Гоген, Джозеф А .; Тэтчер, Джеймс В.; Вагнер, Эрик Г.; Райт, Джесси Б. (1977). «Семантика исходной алгебры и непрерывные алгебры» . Журнал АКМ . 24 (1): 68–95. дои : 10.1145/321992.321997 . S2CID 11060837 .

[Mosses1996-9] Моссес, Питер Д. (1996). Теория и практика семантики действия (Доклад). Отчет БРИКС RS9653. Орхусский университет .

[10] Дерансар, Пьер; Журдан, Мартен; Лорхо, Бернар (1988). «Грамматики атрибутов: определения, системы и библиография . Конспекты лекций по информатике 323. Springer-Verlag . ISBN». 9780387500560 .

[Lawvere1963-11] Ловер, Ф. Уильям (1963). «Функториальная семантика алгебраических теорий» . Труды Национальной академии наук Соединенных Штатов Америки . 50 (5): 869–872. Бибкод : 1963PNAS...50..869L . дои : 10.1073/pnas.50.5.869 . ПМК 221940 . ПМИД 16591125 .

[12] Анджей Тарлецкий; Род М. Берстолл ; Джозеф А. Гоген (1991). «Некоторые фундаментальные алгебраические инструменты для семантики вычислений: Часть 3. Индексированные категории» . Теоретическая информатика . 91 (2): 239–264. дои : 10.1016/0304-3975(91)90085-G .

[13] Бэтти, Марк; Мемариан, Кайван; Ниенхейс, Киндилан; Пишон-Фарабод, Жан; Сьюэлл, Питер (2015). «Проблема семантики параллелизма языка программирования» (PDF) . Труды Европейского симпозиума по языкам и системам программирования . Спрингер . стр. 283–307. дои : 10.1007/978-3-662-46669-8_12 .

[Abramsky2009-14] Абрамский, Самсон (2009). «Семантика взаимодействия: введение в семантику игры». У Эндрю М. Питтса; П. Дюбьер (ред.). Семантика и логика вычислений . Издательство Кембриджского университета. стр. 1–32. дои : 10.1017/CBO9780511526619.002 . ISBN 9780521580571 .

[Dijkstra1975-15] Дейкстра, Эдсгер В. (1975). «Защищенные команды, неопределенность и формальный вывод программ» . Коммуникации АКМ . 18 (8): 453–457. дои : 10.1145/360933.360975 . S2CID 1679242 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]