3. Аксиоматическая семантика

Если операционная семантика предназначена в основном для того, чтобы чётко зафиксировать правила поведения исполнителя программы, то аксиоматическая (дедуктивная) семантика предназначена в основном для того, чтобы чётко зафиксировать правила поведения исполнителя при доказательстве свойств программ (наиболее интересное из таких свойств - свойство давать определённые результаты при определённых входных данных).

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

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

В отличие от операционной семантики дедуктивная семантика отказывается от того, чтобы связывать смысл конструкций языков программирования с каким-либо способом проведения вычислений. Таким образом, она абстрагируется от ряда деталей вычислений, несущественных для понимания смысла программы, и дает возможность говорить об абстрактных свойствах программ. Тем не менее, дедуктивная семантика в основном ориентирована на императивное программирование.[2]

4. Трансляционная семантика

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

В общем случае трансляционный подход может использоваться и для языков высокого уровня. В качестве языка, на который осуществляется перевод, может быть выбран некоторый математический язык (например, язык -исчисления), некоторый другой язык программирования (например, язык Алмо для языков описания алгоритмов или язык Паскаль для языка Сетл) или конкретный машинный язык. Таким образом, транслятор для языка высокого уровня на конкретный машинный язык становится семантическим определением языка.[3]

5. Выводы по методам определения семантики

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

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