197-577-902

Лекции по информатике - Метод инвариантной функции

Метод инвариантной функции является частным случаем метода инварианта цикла.

В данном случае х = х0 и необходимо вычислить f(x0). При этом
I = {множество x | f(x) = f(x0)}
P = {множество x | f(x) вычисляется легко}.

Построим преобразование Т – инвариантное относительно I, а в качестве условия окончания примем само значение P(Q = P).

Схема программы:

x:= x0;
while not p(x) do
  x:= T(x);
result:= f(x);

Для доказательства правильности достаточно доказать, что цикл выполнится за конечное число шагов.

Напишем программу иллюстрирующую данный метод.

Пусть x = (a, b), а f(x) = Н.О.Д.(a, b). Необходимо вычислить Н.О.Д.(a, b).

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

a:= a0;
b:= b0; { >=0 }
while (a>0) and (b>0) do
  if a > b then
    a:= a - b
  else
    b:= b – a;
result := a+b;

Условием выхода из цикла является равенство 0 либо a, либо b, поэтому сумма этих чисел будет нам давать то из чисел которое не равно 0