Тема 6. Семантическая теория программ
108)Формальное описание результата,
который должен быть получен при реализации
программы на допустимой области изменения
исходных данных, называется …спецификация
109)Формальное доказательство правильности
программы в соответствии с заданной
спецификацией называется …верификация
110)Здесь смысл программы и отдельных ее
конструкций задается некоторым четко
описанным множеством операторов, которые
могут быть реализованы на некоторой
реальной или виртуальной машине, этот
подход называется …операционная
семантика
111)Семантику каждой синтаксической
конструкции языка задают в виде аксиом,
которым должны удовлетворять исходные
данные, и правил вывода, с помощью которых
может быть получен результат (как
теорема, которая вытекает их аксиом с
помощью правил вывода), то есть эта
семантика является расширением
математической теории исчисления
предикатов, которая в математике
используется для доказательства теорем,
этот подход называется …аксиоматическая
семантика
112)Для создания семантической модели
программы необходимо разработать
правила, с помощью которых для каждого
оператора S и заданного постусловия R
можно найти слабейшее предусловие
wp(S,R), такие правила называются
…преобразователями предикатов
