Название: Доказательство правильности программ - Конспект лекций (Веретельникова Е.Л.)

Жанр: Экономика

Просмотров: 1604


       к программам для вычислительных машин

 

Иногда не совсем ясно, доказываем ли мы справедливость S(n) для всех n, удовлетворяющих условию n0 £ n £ m0 или условию

n0 £ n. В такой ситуации можно добиться успеха, даже и не зная, с каким из случаев имеешь дело. Например, при доказательстве правильности программы иногда необходимо доказать справедливость некоторого высказывания S в те моменты, когда выполнение программы достигает некоторой определенной точки. Можно попытаться доказать это методом индукции по n – числу «проходов» через данную точку программы. Однако мы можем и не знать точно, сколько раз проходим через эту точку: это зависит от данных, используемых при выполнении программы. Мы можем проходить через нее и конечное (m0), и бесконечное число раз (если программа не заканчивается из-за ошибки). Таким образом, можно попытаться доказать справедливость S(n) для n, удовлетворяющих условию 1 £ n £ m0 или условию 1 £ n. В любом случае мы можем получить результат, не зная, с каким вариантом имеем дело. Мы убеждаемся в справедливости S(n) при каждом проходе через определенную точку, если можем:

1) доказать, что справедливо S(1), т.е. справедливо высказывание S при первом проходе через точку;

2) доказать, что если справедливо S(n) (т.е. при n-м проходе через точку), то справедливо и S(n + 1), если мы, конечно, попадем в точку в (n + 1)-й раз.

Если мы проходим через точку только m0 раз, то значения n, для которых второе положение, возможно, справедливо, это те значения n, при которых мы можем попасть в точку (n + 1)-й раз, т.е. значения, удовлетворяющие условию n0 £ n £ m0–1. Если же мы проходим через точку бесконечное число раз, то значения n, для которых может быть справедливо второе положение, это значения, удовлетворяющие условию 1 £ n. Таким образом, если мы докажем оба положения, то тем самым с помощью простой восходящей или простой индукции мы докажем справедливость высказывания S(n) для всех требуемых значений n вне зависимости от того, какой вариант встречается в действительности.