Чтобы немного расширить ответ Майкла Мэдсена, примером может служить поведение оператора ++. Неформально мы описываем оператор, используя простой английский. Например:
Если x является переменной типа int, ++x приводит к увеличению x на единицу.
(я предполагаю, что нет целочисленных переполнений, и что ++x ничего не возвращает)
В формальной семантике (и я собираюсь использовать операционную семантику) у нас будет немного работы. Во-первых, нам нужно определить понятие типов. В этом случае я предполагаю, что все переменные имеют тип int. На этом простом языке текущее состояние программы может быть описано хранилищем, которое представляет собой отображение переменных на значения. Например, в какой-то момент в программе x может быть равно 42, а y равно -5351. Хранилище может использоваться как функция - например, если в хранилище s есть переменная x со значением 42, то s(x) = 42.
В текущее состояние программы также включены остальные операторы программы, которые мы должны выполнить. Мы можем связать это как <C, s>, где 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}>
Надеюсь, это дает вам идею. Обратите внимание, что это только один пример формальной семантики - наряду с операционной семантикой, есть аксиоматическая семантика (которая часто использует логику Хоара) и денотационная семантика, и, вероятно, еще много, с чем я не знаком.
Как я уже упоминал в комментарии к другому ответу, преимущество формальной семантики состоит в том, что вы можете использовать их для доказательства определенных свойств вашей программы, например, ее завершения. Помимо того, что ваша программа не демонстрирует плохое поведение (например, отсутствие завершения), вы также можете доказать, что ваша программа ведет себя так, как требуется, доказав, что ваша программа соответствует заданной спецификации. Сказав это, я никогда не находил идею указать и проверить программу настолько убедительной, поскольку я обнаружил, что спецификация, как правило, представляет собой программу, переписанную в логике, и поэтому спецификация с такой же вероятностью будет содержать ошибки.