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

Эта статья включает в себя список общих ссылок , но он остается в значительной степени непроверенным, поскольку в нем отсутствует достаточное количество соответствующих встроенных ссылок . Пожалуйста, помогите улучшить эту статью, добавив более точные цитаты. ( Август 2020 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения )

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

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

если  1  ==  1,  то S1 иначе S2

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

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

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

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

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

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

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

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

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

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

Варианты [ править ]

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

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

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

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

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

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

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

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

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

• Вычислительная семантика
• Формальная семантика (логика)
• Формальная семантика (лингвистика)
• Онтология
• Онтология (информатика)
• Семантическая эквивалентность
• Семантическая технология

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

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

Учебники