Открытые проблемы

Repeat

Begin

Begin

Примеры

Приклад. Розглянемо застосування методу a) теореми 6.2 для доведення інваріантності рівності програми, що обчислює найменше число Фібоначчі, більше, ніж .

Procedure Fib(N: Integer; var x: Integer);

var y: Integer;

x:= 1; y:= 1;

While x < N do Begin

x:= x + y;

y:= x - y

End {Invariant: (x^2 - x*y - y^2)^2 - 1}

End;

Побудуємо словник операторів:

Побудуємо регулярний вираз програми:

Послідовне застосування обчислюючи операторів у циклі перетворимо в один оператор Регулярний вираз програми при цьому спроститься: . Інваріант програми представимо у вигляді добутку

. Далі,

Будуємо . . Знаходимо номер стабілізації ланцюжка ідеалів

.

Обчислимо

=

Отже, . Таким чином, і . Доведено, що - інваріант циклу. Відзначимо, що якщо - інваріант циклу а - тіло циклу, то - також інваріант циклу. Цей факт можна використовувати. Наприклад, якщо ідеал інваріантів циклу породжується одним поліномом ланцюжок ідеалів обірветься вже на першому кроці. У противному випадку отримаємо новий інваріант.

Нехай При перетвореннях циклу переходить в , а - в . Таким чином, ідеал інваріантів цього прикладу не є простим. Він розкладається у перетин простих ідеалів, породжених відповідно поліномами та .

Далі, обчислюємо . Отримаємо . Тому

Для доведення інваріантності треба перевірити, що Підставляючи в , переконуємося в цьому:

Приклад Генерація інваріантів методом невизначених коефіцієнтів. Процедура цього приклада здійснює поворот точки на кут доти, поки вона не потрапить в -околицю свого початкового положення .

Procedure Rotation (a, b: Real; e: Real; var x, y: Real);

var u, v: Real;

x:= a; y:= b;

u:= (4/5)*x - (3/5)*y;

v:= (3/5)*x + (4/5)*y;

x:= u; y:= v;

until Sqr((x-a)) + Sqr(y-b) < e;

end;

Cформуємо cловник операторів, редукуючи оператор у тілі циклу до виду

Програму представлено регулярним виразом .

Будемо шукати інваріант у вигляді однорідного поліному 2-ой ступені від змінних .

(6.1)

На практиці можна використовувати метод, намічений в цьому й наступному прикладах. Відзначимо, що обчислення уздовж будь-якого шляху програми, що виконуються для конкретних числових значень вхідних параметрів, приводять до лінійних рівнянь від невизначених коефіцієнтів . Розглянемо обчислення уздовж шляху

Покладемо

. Одержимо: (6.2)

. Одержимо: (6.3)

. Одержимо: (6.4)

Виключаючи з (6.1) , отримаємо:

(6.5)

Рівняння (6.2) - (6.4) лінійно незалежні. Однак, подальші обчислення показують, що рівняння, отримані при інших початкових значеннях уздовж шляху _, залежать від них. Таким чином, можливості отримання нових залежностей з використанням шляху вичерпані. Розглянемо обчислення уздовж шляху . Покладемо . З (6.5) отримаємо:

(6.6)

Знаходячи з (6.6) коефіцієнт C, отримаємо:

(6.7)

Покладемо . З (6.7) отримаємо:

(6.8)

Знаходячи з (6.8) коефіцієнт , отримаємо:

Нарешті, методом a) теореми 6.2 переконаємося в тому, що - інваріант програми.

Инварианты рационально определенных программ

В [3] отмечено, что алгоритмы теоремы 2 могут быть модифицированы для рационально определенных программ. С этой целью можно рассмотреть алгоритм решения задачи 2 в случае, когда в операторе X:= H(X)

H(X) = (h₁(X), …, h_n(X))h_i(X) = r_i(X)/s_i(X),

причем правые части в этом операторе – несократимые дроби.

Для этого множеству X = <x₁, …, x_n > поставим в соответствие набор Z = < z₁, …, z_n >, переменные которого играют роль вспомогательных. Далее, рассмотрим набор полиномов

f₁(Z), …, f_k(Z), x₁*s₁(Z) - r₁(Z), …, x_n*s_n(Z) - r_n(Z) (11)

Построим базис Гребнера этого набора, элиминируя переменные набора Z. Полученный базис Гребнера g₁(X), …, g_k (X) является решением задачи 2.

Аналогичные рассуждения можно применить и в случаях, когда правые части вычисляющих операторов содержат алгебраические иррациональности (например, функции квадратных корней).

- Проблема построения базиса .

- Проблема построения базиса векторногно пространства для программ с рекурсивными вызовами процедур. Эти программы определяются к.с. грамматиками.

II. Полиномиальные инварианты линейных циклов

Дата добавления: 2014-01-20