Формальные методы тесно связаны с математическими техниками
спецификаций, верификацией и доказательством правильности программ.
Эти методы содержат математическую символику, формальную нотацию и
аппарат вывода. Правила доказательства являются громоздкими и
поэтому на практике редко используются рядовыми программистами.
Однако с теоретической точки зрения они развивают логику применения
математического метода индукции при проверке правильности программ.
На основеспецификации программ проводится частичное и полное
доказательство правильности программ [6.4, 6.5].
Под доказательством частичной правильности понимается проверка
выполнения свойств данных программы с помощью утверждений, которые
описывают то, что должна получить эта программа, когда закончится
ее выполнение в соответствии с условиями заключительного
утверждения. Полностью правильной программой по отношению к ее
описанию и заданным утверждениям будет программа, если она частично
правильная и заканчивается ее выполнение при всех данных,
удовлетворяющих ей.
Для доказательства частичной правильности используется метод
индуктивных утверждений, сущность которого состоит в следующем.
Пусть утверждение связано с началом программы, - с конечной точкой
программы и утверждение отражает некоторые закономерности значений
переменных, по крайней мере, в одной из точек каждого замкнутого
пути в программе (например, в циклах). Если при выполнении
программа попадает в -ю точку и справедливо утверждение , а затем
она проходит от точки к точке , то будет справедливо утверждение
.
Теорема 6.1. Если выполнены все действия метода индуктивных
утверждений для программы, то она частично правильна относительно
утверждений , , .
Требуется доказать что, если выполнение программы закончится, то
утверждение будет справедливым. По индукции, при прохождении точек
программы, в которых утверждение будет справедливым, то и -я точка
программы будет такой же. Таким образом, если программа прошла
-точку и утверждения и справедливы, то тогда, попадая из -ой точки
в точку, утверждение будет справедливым, что и требовалось
доказать.
Методы доказательства правильности программ
106
0
1 минута
Темы:
Понравилась работу? Лайкни ее и оставь свой комментарий!
Для автора это очень важно, это стимулирует его на новое творчество!