3. Метод индуктивных утверждений как обобщение метода доказательства правильности с использованием индукции. Верификация программ.

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

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

Сущность каждой программы можно представить описаниями отношений между входными и выходными данными. Эти отношения формализуются 1 программной спецификации. В реальных разработках формализация этих взаимосвязей является неплохой, и часть отношений уточняется в процессе разработок программ. Такие не полностью определённые недостаточны для доказательства корректности программ. Только при полной и точной формализации всех условий и связей между входными и результирующими данными появляется возможность их использования для автоматической верификации.

Метод индуктивных утверждений.

Для изучения этого метода программа снабжается утверждениями о свойствах её переменных в нкоторых точках:

a)      Входные переменные не меняются в процессе исполнения программ;

b)      Описываются состояния переменных в промежуточных точках;

c)      Выходные переменные описываются с помощью отношениями между переменными после завершения программы.

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

Для верификации программ необходимо три языка:

        Язык записи текстов программ;

        Язык формулировки условий верификации;

        Язык формирования и доказательства корректности.

 

Так как эти языки различаются в значительной степени, то это обстоятельство является одним из применения верификации.

 Доказательство корректности имеет следующие преимущества:

 1.      Представляет собой чёткий формализованный процесс.

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

3.      проясняет промежуточные результаты вычислений. Выписывании выражений заставляет программиста четко сформировать свои предположения о результатах вычислений в выбранных точках программы.

4.      Выявляет зависимости. В процессе доказательства программ начинает понимать какие предположения о входных данных не явно испытывается в различных частях программы.

  Недостатки метода:

 1.      Сложность; даже для небольших простых программ выкладки очень сложны, что может привести к ошибкам.

2.      Ошибки, Из-за сложности метода легко допустить ошибки и при формировании доказываемых утверждений и при доказательстве.

3.      Трудности работы с массивами.

4.      Отсутствие мощного математического аппарата.

5.      Высокая трудоёмкость. Для проверки программы требуется затраты труда, чем для её написания (в 2 – 6 раз).

6.      Отсутствие выразительности. Часто нелегко сформировать выгодно утверждение для того что интуитивно представляется очень простым вычислением:

7.      Трудность понимания.

8.      Необходимость обучения. Для применении этого метода требуется длительное обучение и тренировка.