Основы офисного программирования и язык VBA

         

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


Мы уже говорили, что отладка, основанная на построении системы тестов, не может доказать правильность программы. Поэтому в теоретическом программировании были предприняты большие усилия по разработке методов доказательства правильности программ, такие же строгие, как и методы доказательства правильности теорем. На практике эти методы не получили широкого распространения по двум причинам. Во-первых, построить доказательство правильности программы сложнее, чем написать саму программу. Во-вторых, ошибки в доказательстве столь же возможны, как и в самой программе. Тем не менее, знание основ доказательства правильности программ должно быть частью образования программиста. Умение строго доказывать правильность простых программ помогает программисту лучше понять, как следует разрабатывать корректно работающие, сложные программы. Не ставя целью сколь либо полный обзор этого важного направления, остановимся лишь на самом понятии правильности программы. Действительно, мы многократно использовали этот термин, но что значит правильно (корректно) работающая программа? Вот одно из возможных определений. Пусть P(X,Y) - программа, с заданными входными данными X и результатами Y. Предикат Q(X), определенный на входных данных, будем называть предусловием программы P, а предикат R(X,Y), связывающий входные и выходные переменные будем называть постусловием программы P. Будем также предполагать, что в ходе своей работы программа не меняет своих входных переменных X.

Программа P(X,Y) корректна по отношению к предусловию Q(X) и постусловию R(X,Y), если из истинности Q(X) до начала выполнения программы следует, что, будучи запущенной, программа завершит свою работу и по ее завершению будет истинным предикат R(X,Y). Условие корректности записывают в виде триады (триады Хоора) - Q(X) {P(X,Y)} R(X,Y)

Уже из этого определения становится ясно, что говорить о правильности следует не вообще, а по отношению к заданным спецификациям, например, в виде предусловия и постусловия. Доказать правильность триады для сложных программ, как уже говорилось, довольно сложно. Один из методов (метод Флойда) состоит в том, что программа разбивается на участки, размеченные предикатами - Q1, Q2, …QN, R. Первый из предикатов представляет предусловие программы, последний - постусловие. Тогда доказательство корректности сводится к доказательству корректности последовательности триад:

Q1{P1}Q2; Q2{P2}Q3; …QN{PN}R

Нетрудно видеть, что введение Assert - утверждений является отражением метода Флойда. Хотя использование этих утверждений не предполагает проведения строгого доказательства, но это практически реализуемая попытка в этом направлении. Все что может быть сделано для повышения надежности программы, должно быть сделано.



Содержание раздела