Interested Article - Семантика (программирование)

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

Общий смысл

Семантика языка — это смысловое значение слов. В программировании — начальное смысловое значение операторов , основных конструкций языка и т. п.

Пример:

Первый код: 
i=0; while(i<5){i++;}

Второй код: 
i=0; do{i++;} while(i<=4);

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

<i></i>
<em></em>

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

Подходы

Операционная семантика ( англ. operational semantics ) используется для синтаксических понятий языка. В ней функции рассматриваются как текстуальные правильно построенные определения, обеспечивающие применение к аргументу, а не как функции в математическом понимании этого термина.
Существует классификация различных видов операционной семантики:

Аксиоматическая семантика — семантику каждой синтаксической конструкции языка можно определить как некий набор аксиом или правил вывода, который можно использовать для вывода результатов выполнения этой конструкции. Чтобы понять смысл всей программы, эти аксиомы и правила вывода следует использовать так же, как при доказательстве обычных математических теорем. В предположении, что значения входных переменных удовлетворяют некоторым ограничениям, аксиомы и правила вывода могут быть использованы для получения ограничений на значения других переменных после выполнения каждого оператора программы. Когда программа выполнена, получаем доказательство того, что вычисленные результаты удовлетворяют необходимым ограничениям на их значения относительно входных значений. То есть, доказано, что выходные данные представляют значения соответствующей функции, вычисленной по значениям входных данных.

Денотационная семантика ( англ. denotational semantics ) выражениям в программе ставит в соответствие настоящие математические объекты , то есть, выражения обозначают ( англ. to denote — откуда «денотационная») их величины . Важнейшие, в том числе пионерские, результаты построения денотационных семантик получены в работах Д. Скотта (Dana Scott) и К. Страчей (Christopher Strachey) в конце 1960-х — начале 1970-х в Оксфордском университете . Скотт первым построил модель λ-исчисления, основанную на представлении о полном частично упорядоченном множестве. Для этого им были использованы функции, непрерывные на таком множестве.

Интерпретационная семантика — описание операционной семантики конструкций в терминах языков программирования низкого уровня ( язык ассемблера , машинный код ). Этот способ позволяет выявлять медленно выполняемые участки программы, и зачастую используется в соответствующих фрагментах систем программирования в целях оптимизации кода программ .

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

Трансформационная семантика — описание операционной семантики конструкций языка в терминах этого же языка. Трансформационная семантика является основой метапрограммирования .

Предметом постоянного интереса и исследования является построение систем доказательства корректности, или правильности программ. Наиболее разработанными оказались системы доказательства для случая корректности функциональных программ, которые восходят к системе LCF Робина Милнера и системе Р. Бойера (R. Boyer) и Дж. Мура (J. Moore).

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