Методы и средства инженерии программного обеспечения
Модель формального доказательства конкретности программы - часть 5
Иными словами, выполнение исходных условий обеспечена соответствующим преобразованием массива и порядком их выполнения. Доказано, что выполнение программы завершено успешно.
Из этого утверждения генерируется серия теорем, которые доказываются. Начиная с первого утверждения и переходя от одного преобразования к другому, вырабатывается путь вывода, который состоит в том, что если одно утверждение есть истинное, то есть истинно и другое.
Другими словами, если первое утверждение – А1 и первая точка преобразования – А2 , то первой теоремой есть: А1 ® А2..
Если А3 есть такой точкой преобразования, то второй теоремой будет: А2 ® А3.
Таким образом, формулируется общая теорема:
Аі ® Аj,где Аі и Аj – смежные точки преобразования.
Последняя теорема формулируется так, что условие «истинное» в последней точке и отвечает истинности выходного утверждения: Аk ® Аend.
Соответственно, можно возвратиться потом к точке преобразования Аend и к
предшествующей точке преобразования. Доказали, что Аk ® Аend , а значит и Аj ® Аj +1 и так далее, пока не получим, что А1 ® А0
.
Результат любого другого подхода к доказательству правильности будет аналогичный.
4. Чтобы доказать, что программа корректная, необходимо последовательно расположить все части, которые начинаются с А1 и заканчиваются Аend. Последовательность этих частей определяет, что истинность входного условия обеспечивает истинность выходного условия.
5. После идентификации всех частей проверяется истинность каждой части программы с утверждением, что входные утверждения являются следствием выходного утверждения, которые отвечают преобразованиям ее частей. Доказательство программы завершено.
