Автор работы: Пользователь скрыл имя, 20 Марта 2013 в 15:47, реферат
Рассмотрим формальные постановки задач анализа корректности.
Введем ограничение: будем рассматривать программы, начинающиеся оператором START (первый выполняемый оператор) и заканчивающиеся оператором STOP (последний выполняемый оператор).
Спецификацию программы Prgm будем определять путем приписывания индуктивных утверждений точкам разреза графа потоков управления программы (точкам между операторами программы).
Основные задачи анализа корректности программ ……..………………......
.… 2
Метод индуктивных утверждений ……………………………….….……....
…. 7
Анализ завершения последовательных программ ……………...….………..
. 13
Основные концепции формализации семантики программ, аксиоматическая система Хоара ……………………………………………...
. 16
Автоматическая генерация и доказательство условий корректности .….…
. 21
Специфика верификации недетерминированных и параллельных программ ……………………………………………………………………….
.. 24
Литература …………………………………...…………