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



         

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


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

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

Другими словами, если первое утверждение – А1  и первая точка преобразования  – А2 , то  первой теоремой есть:  А1   ® А2..

Если А3 есть такой точкой преобразования, то  второй теоремой будет: А2 ® А3.

Таким образом, формулируется  общая теорема:

 Аі  ® Аj,где  Аі  и  Аj    – смежные точки преобразования.

          

Последняя теорема формулируется так, что  условие «истинное» в последней точке и отвечает истинности выходного утверждения:     Аk  ®  Аend.

Соответственно, можно возвратиться потом  к точке преобразования Аend    и к

предшествующей точке преобразования.  Доказали, что      Аk  ® Аend , а значит и  Аj ® Аj +1  и так далее, пока не получим, что   А1   ® А0

Результат любого  другого подхода к доказательству правильности будет  аналогичный.

 

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

 

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




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