Основные выводы и результаты. · Операционная семантика, сводится к описанию смысла программы посредством выполнения ее операторов на реальной или виртуальной машине.

· Операционная семантика, сводится к описанию смысла программы посредством выполнения ее операторов на реальной или виртуальной машине.

· Операционная семантика является эффективной до тех пор, пока описание языка остается простым и неформальным. Она зависит от алгоритмов, а не от математики.

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

· Аксиоматическое определение семантики оператора дается в виде правила, описывающего, как для любого заданного постусловия R можно вывести соответствующее слабейшее предусловие wp(S, R).

· Если для каждого оператора языка по заданным постусловиям можно вычислить слабейшее предусловие, то для программ на данном языке может быть построено корректное доказательство.

· Основная теорема инвариантности для цикла:

(P AND wp(DO, T)) => wp(DO, P AND NOT BB).

· Аксиоматическая семантика является мощным инструментом для исследований в области доказательств правильности и анализа программ. Однако ее полезность при описании содержания языков программирования весьма ограничена. Трудно построить «множество основных аксиом, достаточно ограниченное для того, чтобы избежать противоречий, но достаточно богатое для того, чтобы служить отправной точкой для доказательства высказываний о программах» (Э. Дейкстра).

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

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

· Денотационные описания достаточно сложны, но они дают великолепный метод краткого описания языка.

· Декларативная семантика применяется в языках логического программирования, в которых программы состоят из объявлений, а не из операторов. Эти объявления являются высказываниями (операторами в символьной логике).

· Декларативная семантика значительно проще, чем семантика императивных языков. Она не требует для проверки отдельного оператора рассмотрения его контекста, локальных объявлений или последовательности выполнения программы.

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

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

· Процесс доказательства на основе метода индуктивных высказываний Флойда и Наура настолько формализуем, что может выполняться на вычислительной машине.

· Метод верификации Хоара и Дейкстры основан на формальном выводе программ из математической постановки задачи на основе исчисления предикатов первого порядка.

· Правила верификации Хоара определяют достаточные предусловия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желаемым постусловиям.