Информатика


Элементы доказательного программирования - часть 3


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

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

В качестве примера проведем анализ результатов алгоритма, со­стоящего из трех присваиваний.

алг «у = х5»                Результаты                 Утверждения

нач

v

:= х×х                        v1 = х×х            Þ        v1 = x2

v := v×v                        v2

= v1×v1          Þ        v2 = x4

у := v×x                        у = v2×x            Þ        у = х5

кон

Справа от алгоритма приведены результаты выполнения присва­иваний. Результатом первого присваивания v := х×х будет значение v1

= х×х переменной v. Результат следующего присваивания v := v×v - второе значение переменной v, равное v2 = v1×v1 . Результатом треть­его присваивания у := v×x будет значение у = v2×x .

На основе приведенных рассуждений, можно сделать три утверж­дения о промежуточных и конечных результатах вычислений:

Результаты                             Утверждения

{ v1 = х×х                     Þ        v1 = х2

{ v2 = v1×v1                  Þ        v2 = x4

{ у = v2×x                     Þ        у = х5

Таким образом можно высказать окончательное

Утверждение. Конечным результатом выполнения будет

у = х5 для любых значений х.

Доказательство. Исходя из описания результатов выполнения присваиваний значение у будет равно

у = v2×x = (v1×v,)×x = ((х×х).(х×х))) ×х = x5.

Что и

требовалось доказать.

Техника анализа и

доказательства правильности алгоритмов и программ во многом совпадает с техникой доказательства любых других утверждений и состоит в применении следующих четырех приемов:




Начало  Назад  Вперед



Книжный магазин