Что такое “формальная семантика”?

Чтобы немного расширить ответ Майкла Мэдсена, примером может служить поведение оператора ++. Неформально мы описываем оператора простым английским языком. Например:

Если x является переменной типа int , ++ x заставляет x увеличиваться на единицу.

(Я предполагаю, что нет целочисленных переполнений и что ++ x ничего не возвращает)

В формальной семантике (и я собираюсь использовать операционную семантику) мы ' Мне нужно немного поработать. Во-первых, нам нужно определить понятие типов. В этом случае я предполагаю, что все переменные имеют тип int . На этом простом языке текущее состояние программы может быть описано хранилищем, которое представляет собой отображение переменных в значения. Например, в какой-то момент программы x может быть равно 42, а y равно -5351. Хранилище можно использовать как функцию - так, например, если хранилище s имеет переменную x со значением 42, то s (x) = 42 .

В текущее состояние программы также включены оставшиеся операторы программы, которую мы должны выполнить. Мы можем связать это как , где C - это оставшаяся программа, а s - это хранилище.

Итак, если у нас есть состояние <++ x, {x -> 42, y -> -5351}> , это неформально состояние, в котором единственной оставшейся командой для выполнения является ++ x , переменная x имеет значение 42, а переменная y имеет значение -5351 .

Затем мы можем определить переходы от одного состояния программы к другому - мы описываем, что происходит, когда мы делаем следующий шаг в программе. Итак, для ++ мы могли бы определить следующую семантику:

<++x, s> --> <skip, s{x -> (s(x) + 1)>

Несколько неформально, выполнив ++ x , следующая команда будет skip , которая не имеет никакого эффекта, и переменные в хранилище не изменяются, за исключением x , который теперь имеет значение плюс один, которое было изначально. Еще предстоит проделать некоторую работу, например, определить нотацию, которую я использовал для обновления магазина (чего я не сделал, чтобы этот ответ не стал еще длиннее!). Итак, конкретным примером общего правила может быть:

<++x, {x -> 42, y -> -5351}> --> <skip, {x -> 43, y -> -5351}>

Надеюсь, это дает вам идею. Обратите внимание, что это всего лишь один пример формальной семантики - наряду с операционной семантикой есть аксиоматическая семантика (которая часто использует логику Хоара) и денотационная семантика, и, вероятно, многое другое, с чем я не знаком.

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

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

Эта страница из A Practical Introduction to Denotational Semantics является хорошим введением в то, как [денотативная] семантика связана с синтаксисом. В начале книги также дается краткая история других, неденотативных подходов к формальной семантике (хотя ссылка на википедию, которую дал Майкл, содержит еще больше деталей и, вероятно, является более актуальной).

С сайта автора:

Модели для семантики не были прижились в той же степени, что БНФ и его потомки в синтаксисе. Это может быть связано с тем, что семантика кажется, просто труднее, чем синтаксис. Наиболее успешной системой является денотативная семантика, которая описывает все особенности, встречающиеся в императивных языках программирования и имеет прочную математическую основу. (До сих пор ведутся активные исследования в области систем типов и параллельного программирования.) Многие многие денотативные определения могут быть выполняться в виде интерпретаторов или переводиться в "компиляторы", но это еще не привело к появлению пока не привело к созданию генераторов эффективных компиляторов, что может быть еще одной причиной что денотационная семантика менее популярна, чем БНФ.