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

Question

Я читаю очень глупую статью, и она продолжает говорить о том, как Джотто определяет "формальную семантику".

Giotto имеет формальную семантику, которая определяет значение переключателей режимов, взаимодействия между задачами и взаимодействия с программной средой.

Я на грани, но просто не могу понять, что означает "формальная семантика".

Answer 1

Формальная семантика описывает семантику - ну, формально - используя нотацию, которая однозначно выражает смысл вещей.

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

Язык программирования может иметь как формальную, так и неформальную семантику - тогда неформальная семантика будет служить "текстовым" объяснением формальной семантики, а формальная семантика будет тем местом, где вы будете искать, если не уверены, что такое неформальное объяснение. действительно значит.

Answer 2

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

Если 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}>

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

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

Answer 3

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

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

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

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

Answer 4

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

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

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

C или C++, с другой стороны, неформально определяются техническими описаниями, хотя существуют научные статьи, которые формализуют аспекты этих языков (например, Майкл Норриш: формальная семантика для C++, https://publications.csiro.au/rpr/pub?pid=nicta:1203), но это часто не попадает в официальные стандарты (возможно, из-за недостатка практичности, особенно из-за сложностей в обслуживании).