Методы доказательства правильности программ

Формальные методы тесно связаны с математическими техниками спецификаций, верификацией и доказательством правильности программ. Эти методы содержат математическую символику, формальную нотацию и аппарат вывода. Правила доказательства являются громоздкими и поэтому на практике редко используются рядовыми программистами. Однако с теоретической точки зрения они развивают логику применения математического метода индукции при проверке правильности программ. На основе спецификации программ проводится частичное и полное доказательство правильности программ [6.4, 6.5].

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

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

Теорема 6.1. Если выполнены все действия метода индуктивных утверждений для программы, то она частично правильна относительно утверждений , , .

Требуется доказать что, если выполнение программы закончится, то утверждение будет справедливым. По индукции, при прохождении точек программы, в которых утверждение будет справедливым, то и -я точка программы будет такой же. Таким образом, если программа прошла -точку и утверждения и справедливы, то тогда, попадая из -ой точки в точку, утверждение будет справедливым, что и требовалось доказать.