Методы и средства инженерии программного обеспечения



         

Общая характеристика формальных методов доказательства - часть 3


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

В общем метод математической индукции разрешает доказать истинность некоторого предположения Р(n), в зависимости от  параметра n,  для всех n ³ n0, и тем самым   доказать случай Р (n0). Истинность Р(n) для любого значения n, доказывает  Р(n+1) и тем самым доказательство истинности Р(n) для всех n ³ n0.  

Этот путь  доказательства используется  для  утверждения А относительно  программы, которая при своем выполнении достигает определенной точки. Проходя через эту точку n раз, можно получить справедливость утверждения А(n), если докажем:

1) что справедливо А(1)  при первом проходе через заданную точку,

2) если справедливо А(n) (при n–проходах через заданную точку), то справедливо и А (n+1) при прохождении через  заданную точку  n+1 раз.

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

 




Содержание  Назад  Вперед