Введение
Математическое изучение смысла языков программирования
В теории языков программирования семантика — это строгое математическое изучение смысла языков программирования. Семантика определяет вычислительное значение синтаксически корректным конструкциям языка программирования. Она тесно связана и часто пересекается с семантикой математических доказательств. Семантика описывает процессы, которые выполняет компьютер при исполнении программы, написанной на данном языке. Это достигается путем описания соотношения между входными и выходными данными программы или объяснения того, как программа будет выполняться на определенной платформе, создавая тем самым модель вычислений.
История
В 1967 году Роберт В. Флойд опубликовал статью "Присвоение значений программам"; его основной целью было "строгий критерий для доказательств о компьютерных программах, включая доказательства корректности, эквивалентности и завершаемости". Флойд далее писал: Семантическое определение языка программирования, в нашем подходе, основывается на синтаксическом определении. Оно должно указывать, какие фразы в синтаксически корректной программе представляют собой команды и какие условия должны быть наложены на интерпретацию в окрестности каждой команды. В 1969 году Тони Хоар опубликовал статью о логике Хоара, вдохновлённую идеями Флойда, которую теперь иногда объединяют термином аксиоматическая семантика. В 1970-х годах возникли термины операционная семантика и денотационная семантика.
A semantic definition of a programming language, in our approach, is founded on a syntactic definition. It must specify which of the phrases in a syntactically correct program represent commands, and what conditions must be imposed on an interpretation in the neighborhood of each command. In 1969, Tony Hoare published a paper on Hoare logic seeded by Floyd's ideas, now sometimes collectively called axiomatic semantics. In the 1970s, the terms operational semantics and denotational semantics emerged.
Описание отношений
По разным причинам может возникнуть необходимость описать отношения между различными формальными семантиками. Например:
Доказать, что конкретная операционная семантика для языка удовлетворяет логическим формулам аксиоматической семантики для этого языка. Такое доказательство демонстрирует, что обоснованно рассуждать об определенной (операционной) стратегии интерпретации, используя определенную (аксиоматическую) систему доказательств. Доказать, что операционная семантика для высокоуровневой машины связана с семантикой для низкоуровневой машины посредством симуляции, при этом низкоуровневая абстрактная машина содержит более примитивные операции, чем высокоуровневая абстрактная машина, определяющая данный язык. Такое доказательство показывает, что низкоуровневая машина "точно реализует" высокоуровневую машину. Также возможно установить связь между несколькими семантиками посредством абстракций, используя теорию абстрактной интерпретации.
To prove that a particular operational semantics for a language satisfies the logical formulas of an axiomatic semantics for that language. Such a proof demonstrates that it is "sound" to reason about a particular (operational) interpretation strategy using a particular (axiomatic) proof system. To prove that operational semantics over a high level machine is related by a simulation with the semantics over a low level machine, whereby the low level abstract machine contains more primitive operations than the high level abstract machine definition of a given language. Such a proof demonstrates that the low level machine "faithfully implements" the high level machine. It is also possible to relate multiple semantics through abstractions via the theory of abstract interpretation.