ПРОГРА́ММ ВЕРИФИКА́ЦИЯ
-
Рубрика: Математика
-
Скопировать библиографическую ссылку:
ПРОГРА́ММ ВЕРИФИКА́ЦИЯ, направление теоретич. программирования, связанное с разработкой и изучением методов доказательства правильности программ, ориентированных на практич. применение.
Программа A частично правильна относительно предусловия P и постусловия Q (обозначение P{A}Q), если, в случае когда P истинно для входных значений переменных и A завершает работу, Q истинно для выходных значений переменных. Программа A тотально правильна относительно P и Q, если выполняется P{A}Q и A завершает работу для входных значений переменных, удовлетворяющих условию P. Для доказательства частичной правильности операторных программ обычно используются модификации метода Флойда, который состоит в следующем. На программы схеме выбираются контрольные точки так, чтобы любой циклич. путь проходил по крайней мере через одну точку. С каждой контрольной точкой ассоциируется спец. условие (индуктивное утверждение или инвариант цикла), которое истинно при каждом переходе через эту точку. С входом и выходом схемы также ассоциируются пред- и постусловия. Затем каждому пути программы между двумя соседними контрольными точками сопоставляется т. н. условие правильности. Выполнение всех условий правильности гарантирует частичную правильность программы.
Один из способов доказательства завершения работы программы состоит во введении в программу дополнит. счётчиков для каждого цикла и в доказательстве их ограниченности в процессе доказательства частичной правильности. Одна из модификаций метода Флойда заключается в построении конечной аксиоматич. системы (т. н. логики Хоара), состоящей из схем аксиом и правил вывода, в которой в качестве теорем выводимы утверждения о частичной правильности программ на языке программирования паскаль. Такая система используется и для задания аксиоматич. семантики паскаля.
Для доказательства правильности рекурсивных программ используется индукция, связанная с определением наименьшей неподвижной точки, а для программ со сложными структурами данных (напр., графами, деревьями) – индукция по структуре данных. В теоретич. исследованиях по логикам Хоара интересуются вопросами их состоятельности и полноты, т. е. обычными свойствами аксиоматизаций в логике. В работах по практич. П. в. рассматриваются вопросы построения удобных языков утверждений о программах, применения ЭВМ для автоматизации процесса П. в. и др.