Верификация
(подтверждение правильности) – состоит в проверке и доказательстве корректности
разработанной программы по отношению к совокупности формальных утверждений,
представленных в спецификации и полностью определяющей связь между входными и
выходными данными этой программы. При этом отношения между переменными н входе
и выходе программы анализируется не в виде значений, как при тестировании, а в
виде описаний их свойств, проявляющихся при любых процессах обработок этих
переменных контролируемой в программе.
Верификация
программы в принципе исключает необходимость её тестирования и отладки, так как
при этом на более высоком уровне понятий и описаний всех переменных,
устанавливается корректность процессов, их обработка и преобразования.
Сущность
каждой программы можно представить описаниями отношений между входными и
выходными данными. Эти отношения формализуются 1 программной спецификации. В
реальных разработках формализация этих взаимосвязей является неплохой, и часть
отношений уточняется в процессе разработок программ. Такие не полностью
определённые недостаточны для доказательства корректности программ. Только при
полной и точной формализации всех условий и связей между входными и
результирующими данными появляется возможность их использования для
автоматической верификации.
Метод индуктивных утверждений.
Для изучения этого
метода программа снабжается утверждениями о свойствах её переменных в нкоторых
точках:
a)
Входные переменные не меняются в процессе исполнения
программ;
b)
Описываются состояния переменных в промежуточных
точках;
c)
Выходные переменные описываются с помощью отношениями
между переменными после завершения программы.
Верификация
состоит в последовательной демонстрации того, что из входных переменных и
преобразований, выполненных на первом шаге следует истинность утверждения,
сформированного в следующей промежуточной точке.
Для
верификации программ необходимо три языка:
·
Язык записи текстов программ;
·
Язык формулировки условий верификации;
·
Язык формирования и доказательства корректности.
Так как эти языки
различаются в значительной степени, то это обстоятельство является одним из
применения верификации.
Доказательство корректности имеет
следующие преимущества:
1.
Представляет собой чёткий формализованный процесс.
2.
Требует анализа. Процесс доказательства
корректности дает возможность
рассматривать части программ, которое в противном случае анализируется лишь
случайно.
3.
проясняет промежуточные результаты вычислений.
Выписывании выражений заставляет программиста четко сформировать свои
предположения о результатах вычислений в выбранных точках программы.
4.
Выявляет зависимости. В процессе доказательства
программ начинает понимать какие предположения о входных данных не явно
испытывается в различных частях программы.
Недостатки
метода:
1.
Сложность; даже для небольших простых программ выкладки
очень сложны, что может привести к ошибкам.
2.
Ошибки, Из-за сложности метода легко допустить ошибки и
при формировании доказываемых утверждений и при доказательстве.
3.
Трудности работы с массивами.
4.
Отсутствие мощного математического аппарата.
5.
Высокая трудоёмкость.
Для проверки программы требуется затраты труда, чем для её написания (в
2 – 6 раз).
6.
Отсутствие выразительности. Часто нелегко сформировать
выгодно утверждение для того что интуитивно представляется очень простым вычислением:
7.
Трудность понимания.
8.
Необходимость
обучения. Для применении этого метода требуется длительное обучение и
тренировка.