Область, связанная со строгим математическим изучением значения языков программирования
В теории языков программирования, семантика - это область, связанная со строгим математическим изучением значения языков программирования. Это достигается путем оценки значения синтаксически действительных строк, определенных конкретным языком программирования, с указанием задействованных вычислений. В таком случае, если оценка будет синтаксически недопустимой строкой, результатом будет невычисление. Семантика описывает процессы, которым следует компьютер при выполнении программы на этом конкретном языке. Это можно показать, описав взаимосвязь между вводом и выводом программы или объяснив, как программа будет выполняться на определенной платформе, тем самым создав модель вычислений.
Формальная семантика, например, помогает писать компиляторы, лучше понимать, что делает программа, и доказывать, например, что следующий ifоператор
if 1 = = 1, тогда S1 иначе S2
имеет тот же эффект, что и S1отдельно.
Содержание
- 1 Обзор
- 2 Подходы
- 3 Варианты
- 4 Описание отношений
- 5 История
- 6 См. Также
- 7 Ссылки
- 8 Дополнительная литература
- 9 Внешние ссылки
Обзор
Область формальной семантики включает в себя все следующее:
- Определение семантических моделей
- Отношения между различными семантическими моделями
- Отношения между различными подходами к значению
- Отношения между вычислениями и лежащими в их основе математическими структурами из таких областей, как логика, теория множеств, теория моделей, теория категорий и т. Д.
Он имеет тесные связи с другими областями информатики, такими как дизайн языков программирования, теория типов, компиляторы и интерпретаторы, проверка программ и проверка моделей.
Подходы
Есть много подходов к формальной семантике ; они относятся к трем основным классам:
- денотационная семантика, при которой каждая фраза в языке интерпретируется как денотация, то есть концептуальное значение, которое можно рассматривать абстрактно. Такие обозначения часто являются математическими объектами, населяющими математическое пространство, но это не является обязательным требованием. В качестве практической необходимости обозначения описываются с помощью некоторой формы математической записи, которая, в свою очередь, может быть формализована как денотационный метаязык. Например, денотационная семантика функциональных языков часто переводит язык в теорию предметной области. Денотационные семантические описания могут также служить в качестве композиционных переводов с языка программирования на денотационный метаязык и использоваться в качестве основы для разработки компиляторов.
- Операционная семантика, при которой выполнение языка описывается напрямую ( а не переводом). Операционная семантика примерно соответствует интерпретации, хотя, опять же, «язык реализации» интерпретатора обычно является математическим формализмом. Операционная семантика может определять абстрактную машину (например, машину SECD ) и придавать смысл фразам, описывая переходы, которые они вызывают в состояниях машины. В качестве альтернативы, как и в случае с чистым лямбда-исчислением, операционная семантика может быть определена с помощью синтаксических преобразований фраз самого языка;
- Аксиоматическая семантика, с помощью которой фразы придают смысл посредством описания применимые к ним аксиомы. Аксиоматическая семантика не делает различий между значением фразы и логическими формулами, которые ее описывают; его смысл - это именно то, что можно доказать с помощью некоторой логики. Каноническим примером аксиоматической семантики является логика Хоара.
Различия между тремя широкими классами подходов иногда могут быть нечеткими, но все известные подходы к формальной семантике используют вышеупомянутые методы или некоторые их комбинации.
Помимо выбора между денотационным, операционным или аксиоматическим подходами, наибольшее разнообразие формальных семантических систем возникает из-за выбора поддерживающего математического формализма.
Варианты
Некоторые варианты формальной семантики включают следующее:
- Семантика действия - это подход, который пытается модулировать денотационную семантику, разделяя процесс формализации на два уровня (макро- и микросемантика) и предопределение трех семантических сущностей (действия, данные и результаты) для упрощения спецификации;
- Алгебраическая семантика - это форма аксиоматической семантики на основе алгебраические законы для описания и рассуждения о семантике программ в формальной манере;
- грамматики атрибутов определяют системы, которые систематически вычисляют "метаданные "(называемые атрибутами) для различных случаев синтаксиса языка. Грамматику атрибутов можно понимать как денотационную семантику, где целевой язык - это просто исходный язык, обогащенный аннотациями атрибутов. Помимо формальной семантики, грамматики атрибутов также использовались для генерации кода в компиляторах и для дополнения обычных или контекстно-свободных грамматик с помощью context- чувствительные условия;
- категориальная (или «функториальная») семантика использует теорию категорий в качестве основного математического формализма. Обычно доказывается, что категориальная семантика соответствует некоторой аксиоматической семантике, которая дает синтаксическое представление категориальных структур. Кроме того, денотационная семантика часто является экземплярами общей категориальной семантики;
- Семантика параллелизма - универсальный термин для любой формальной семантики, описывающей параллельные вычисления. Исторически важные параллельные формализмы включали модель актора и исчисления процесса ;
- семантика игры использует метафору, вдохновленную теорией игр.
- семантикой преобразователя предикатов, разработанный Эдсгер В. Дейкстра, описывает значение фрагмента программы как функцию, преобразующую постусловие в предусловие, необходимое для его установления..
Описание отношений
По ряду причин может возникнуть желание описать отношения между различной формальной семантикой. Например:
- Чтобы доказать, что конкретная операционная семантика для языка удовлетворяет логическим формулам аксиоматической семантики для этого языка. Такое доказательство демонстрирует, что «разумно» рассуждать о конкретной (операционной) стратегии интерпретации с использованием конкретной (аксиоматической) системы доказательства.
- Чтобы доказать, что операционная семантика над машиной высокого уровня связана с имитация с семантикой над машиной нижнего уровня, при этом абстрактная машина нижнего уровня содержит больше примитивных операций, чем определение абстрактной машины высокого уровня данного языка. Такое доказательство демонстрирует, что машина нижнего уровня "точно реализует" машину высокого уровня.
Также возможно связать множественную семантику через абстракции через теорию абстрактной интерпретации.
История
Роберт В. Флойд считается основателем области семантики языков программирования в Флойд (1967).
См. Также
Ссылки
Дополнительная литература
- Учебники
