Семантика (информатика) - Semantics (computer science)

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

Формальная семантика, например, помогает писать компиляторы, лучше понять, что делает программа, и доказать, например, что следующие если заявление

если 1 == 1 тогда S1 еще S2

имеет тот же эффект, что и S1 один.

Обзор

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

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

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

Подходы

Есть много подходов к формальной семантике; они принадлежат к трем основным классам:

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

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

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

Вариации

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

Семантика действия - это подход, который пытается модулировать денотационную семантику, разделяя процесс формализации на два уровня (макро и микросемантика) и предопределяя три семантических объекта (действия, данные и уступки) для упрощения спецификации;
Алгебраическая семантика это форма аксиоматическая семантика на основе алгебраический законы для описания и рассуждения о семантика программы в формальный манера;
Грамматики атрибутов определить системы, которые систематически вычисляют "метаданные " (называется атрибуты) для различных случаев синтаксис языка. Грамматику атрибутов можно понимать как денотационную семантику, где целевой язык - это просто исходный язык, обогащенный аннотациями атрибутов. Помимо формальной семантики, грамматики атрибутов также использовались для генерации кода в компиляторы, и увеличить регулярный или контекстно-свободные грамматики с контекстно-зависимый условия;
Категоричный (или "функториальная") семантика использует теория категорий как основной математический формализм. Обычно доказывается, что категориальная семантика соответствует некоторой аксиоматической семантике, которая дает синтаксическое представление категориальных структур. Кроме того, денотационная семантика часто является экземпляром общей категориальной семантики;
Семантика параллелизма - это универсальный термин для любой формальной семантики, описывающей параллельные вычисления. Исторически важные параллельные формализмы включали Актерская модель и технологические расчеты;
Семантика игры использует метафору, вдохновленную теория игры.
Семантика преобразователя предикатов, разработан Эдсгер В. Дейкстра, описывает смысл фрагмента программы как функцию преобразования постусловие к предварительное условие нужно было его установить.

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

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

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

Также возможно связать множественную семантику через абстракции через теорию абстрактная интерпретация.

История

Роберт В. Флойд считается основателем области семантики языков программирования в Флойд (1967).^[1]

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

использованная литература

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

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

Учебники

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

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

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

внешняя ссылка

Оби, Энтони (2004). Введение в языки программирования. Архивировано 19 июня 2015 года.CS1 maint: BOT: статус исходного URL-адреса неизвестен (ссылка на сайт) Семантика.

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

[1]