Глава 7 Формальная семантика языков программирования
Эта глава отведена обсуждению формальных подходов к описанию семантики языков программирования. Вначале поясняются синтезируемые атрибуты и атрибутные грамматики, которые являются расширениями обычных, синтаксических грамматик на область семантики. Затем дается характеристика операционной семантики, максимально задействующей воображение человека в роли виртуальной машины. Значительное место и внимание уделено аксиоматической семантике — наиболее развиваемому на практике подходу к автоматическому доказательству корректности программы. Рассматривается принятая в нем схема доказательства, использование правил вывода, опирающихся на постусловия и предусловия; приводятся примеры подобных правил для наиболее популярных конструкций языка. В частности, описывается понятие инварианта цикла и исследуются методики его определения. В заключение объясняются основные идеи денотационного подхода к заданию семантики, где во главу угла поставлены рекурсивные функции отображения отдельных конструкций языка в область семантических значений. Демонстрируются примеры функций семантического отображения для чисел, выражений, операторов присваивания и циклов.