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

Для термина «Семантика» см. также другие значения.

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

Общий смысл

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

Пример:

Первый код: 
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-х в Оксфордском университете. Скотт первым построил модель <math>\lambda</math>-исчисления, основанную на представлении о полном частично упорядоченном множестве. Для этого им были использованы функции, непрерывные на таком множестве.

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

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

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

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

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

См. также

• Семантическая паутина
• Онтология (информатика)

Литература

• Калайда В. Т. Теория вычислительных процессов. — Томск: ТУСУР, 2012. — 153 с.

Отрывок, характеризующий Семантика (программирование)

– Ведь это не шутки шутить, – говорил он. – Хорошо, кто один. Одна голова и бедна – так одна, а то ведь тринадцать человек семьи, да все имущество… Довели, что пропадать всем, что ж это за начальство после этого?.. Эх, перевешал бы разбойников…
– Да ну, будет, – говорил другой.
– А мне что за дело, пускай слышит! Что ж, мы не собаки, – сказал бывший исправник и, оглянувшись, увидал Алпатыча.
– А, Яков Алпатыч, ты зачем?
– По приказанию его сиятельства, к господину губернатору, – отвечал Алпатыч, гордо поднимая голову и закладывая руку за пазуху, что он делал всегда, когда упоминал о князе… – Изволили приказать осведомиться о положении дел, – сказал он.
– Да вот и узнавай, – прокричал помещик, – довели, что ни подвод, ничего!.. Вот она, слышишь? – сказал он, указывая на ту сторону, откуда слышались выстрелы.
– Довели, что погибать всем… разбойники! – опять проговорил он и сошел с крыльца.
Алпатыч покачал головой и пошел на лестницу. В приемной были купцы, женщины, чиновники, молча переглядывавшиеся между собой. Дверь кабинета отворилась, все встали с мест и подвинулись вперед. Из двери выбежал чиновник, поговорил что то с купцом, кликнул за собой толстого чиновника с крестом на шее и скрылся опять в дверь, видимо, избегая всех обращенных к нему взглядов и вопросов. Алпатыч продвинулся вперед и при следующем выходе чиновника, заложив руку зазастегнутый сюртук, обратился к чиновнику, подавая ему два письма.
– Господину барону Ашу от генерала аншефа князя Болконского, – провозгласил он так торжественно и значительно, что чиновник обратился к нему и взял его письмо. Через несколько минут губернатор принял Алпатыча и поспешно сказал ему:
– Доложи князю и княжне, что мне ничего не известно было: я поступал по высшим приказаниям – вот…
Он дал бумагу Алпатычу.
– А впрочем, так как князь нездоров, мой совет им ехать в Москву. Я сам сейчас еду. Доложи… – Но губернатор не договорил: в дверь вбежал запыленный и запотелый офицер и начал что то говорить по французски. На лице губернатора изобразился ужас.
– Иди, – сказал он, кивнув головой Алпатычу, и стал что то спрашивать у офицера. Жадные, испуганные, беспомощные взгляды обратились на Алпатыча, когда он вышел из кабинета губернатора. Невольно прислушиваясь теперь к близким и все усиливавшимся выстрелам, Алпатыч поспешил на постоялый двор. Бумага, которую дал губернатор Алпатычу, была следующая:
«Уверяю вас, что городу Смоленску не предстоит еще ни малейшей опасности, и невероятно, чтобы оный ею угрожаем был. Я с одной, а князь Багратион с другой стороны идем на соединение перед Смоленском, которое совершится 22 го числа, и обе армии совокупными силами станут оборонять соотечественников своих вверенной вам губернии, пока усилия их удалят от них врагов отечества или пока не истребится в храбрых их рядах до последнего воина. Вы видите из сего, что вы имеете совершенное право успокоить жителей Смоленска, ибо кто защищаем двумя столь храбрыми войсками, тот может быть уверен в победе их». (Предписание Барклая де Толли смоленскому гражданскому губернатору, барону Ашу, 1812 года.)
Народ беспокойно сновал по улицам.
Наложенные верхом возы с домашней посудой, стульями, шкафчиками то и дело выезжали из ворот домов и ехали по улицам. В соседнем доме Ферапонтова стояли повозки и, прощаясь, выли и приговаривали бабы. Дворняжка собака, лая, вертелась перед заложенными лошадьми.
Алпатыч более поспешным шагом, чем он ходил обыкновенно, вошел во двор и прямо пошел под сарай к своим лошадям и повозке. Кучер спал; он разбудил его, велел закладывать и вошел в сени. В хозяйской горнице слышался детский плач, надрывающиеся рыдания женщины и гневный, хриплый крик Ферапонтова. Кухарка, как испуганная курица, встрепыхалась в сенях, как только вошел Алпатыч.
– До смерти убил – хозяйку бил!.. Так бил, так волочил!..
– За что? – спросил Алпатыч.
– Ехать просилась. Дело женское! Увези ты, говорит, меня, не погуби ты меня с малыми детьми; народ, говорит, весь уехал, что, говорит, мы то? Как зачал бить. Так бил, так волочил!
Алпатыч как бы одобрительно кивнул головой на эти слова и, не желая более ничего знать, подошел к противоположной – хозяйской двери горницы, в которой оставались его покупки.
– Злодей ты, губитель, – прокричала в это время худая, бледная женщина с ребенком на руках и с сорванным с головы платком, вырываясь из дверей и сбегая по лестнице на двор. Ферапонтов вышел за ней и, увидав Алпатыча, оправил жилет, волосы, зевнул и вошел в горницу за Алпатычем.
– Аль уж ехать хочешь? – спросил он.
Не отвечая на вопрос и не оглядываясь на хозяина, перебирая свои покупки, Алпатыч спросил, сколько за постой следовало хозяину.
– Сочтем! Что ж, у губернатора был? – спросил Ферапонтов. – Какое решение вышло?
Алпатыч отвечал, что губернатор ничего решительно не сказал ему.
– По нашему делу разве увеземся? – сказал Ферапонтов. – Дай до Дорогобужа по семи рублей за подводу. И я говорю: креста на них нет! – сказал он.
– Селиванов, тот угодил в четверг, продал муку в армию по девяти рублей за куль. Что же, чай пить будете? – прибавил он. Пока закладывали лошадей, Алпатыч с Ферапонтовым напились чаю и разговорились о цене хлебов, об урожае и благоприятной погоде для уборки.
– Однако затихать стала, – сказал Ферапонтов, выпив три чашки чая и поднимаясь, – должно, наша взяла. Сказано, не пустят. Значит, сила… А намесь, сказывали, Матвей Иваныч Платов их в реку Марину загнал, тысяч осьмнадцать, что ли, в один день потопил.