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

← →
Учащийся (2010-03-10 18:09) [0]

Здравствуйте!Можете объяснить, как доказать корректность работы алгоритма с помощью инвариантов цикла.Допустим линейный поиск:
in:A[], u //массив, искомый элемент
out:i //индекс элемента u в массиве А
begin
i=0;
for j:=1 to length(a) do
if A[j]=u then
i:=j
end;

← →
oldman © (2010-03-10 18:47) [1]

Инвариантом называется логическое выражение, истинное после каждого прохода тела цикла (после выполнения фиксированного оператора) и перед началом выполнения цикла, зависящее от переменных, изменяющихся в теле цикла.[3]

Инварианты используются в теории верификации программ для доказательства правильности выполнения цикла. Порядок доказательства работоспособности цикла с помощью инварианта сводится к следующему:

1.Доказывается, что выражение инварианта истинно перед началом цикла.
2.Доказывается, что выражение инварианта сохраняет свою истинность после выполнения тела цикла; таким образом, по индукции, доказывается, что по завершении цикла инвариант будет выполняться.
3.Доказывается, что при истинности инварианта после завершения цикла переменные примут именно те значения, которые требуется получить (это элементарно определяется из выражения инварианта и известных конечных значениях переменных, на которых основывается условие завершения цикла).
4.Доказывается (возможно — без применения инварианта), что цикл завершится, то есть условие завершения рано или поздно будет выполнено.
5.Истинность утверждений, доказанных на предыдущих этапах, однозначно свидетельствует о том, что цикл выполнится за конечное время и даст желаемый результат.
Также инварианты используют при проектировании и оптимизации циклических алгоритмов. Например, чтобы убедиться, что оптимизированный цикл остался корректным, достаточно доказать, что инвариант цикла не нарушен и условие завершения цикла достижимо.

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

Википедия ©
ЗЫ: Сдавай свой зачет сам!!!

Доказательство корректности алгоритма с помощью инвариантов Найти похожие ветки