Пример 2.

Пример 1.

Основное определение

M = max(a,b) // Постоусловие

Доказать:

B =abs(a) // b²=a²

Доказать:

Определение. Инвариантом программы в контрольной точке называется соотношение между ее переменными, которое выполняется всякий раз, когда процесс вычислений проходит через эту точку, независимо от назальных значений переменных.

Проблема генерации инвариантов циклов в императивных программах была поставлена в работах Р. Флойда [1] и С. Хоара [2] как ключевая проблема процесса анализа свойств программ.

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

I. Алгоритм генерации полиномиальных инвариантов ограниченной степени в императивныхпрограммах

Розглянемо клас програм, для яких алгебра даних є конструктивним полем . Через позначимо множину змінних програми .

Означення. Поліном називається поліноміальним програмним інваріантом програми , якщо для довільного початкового стану пам’яті , якщо програма завершила виконання у заключному стані пам’яті виконується рівність . Рівність називається інваріантною рівністю програми .

ПрикладІнваріант та інваріантна рівність програми

Procedure ModDiv(a, b: Integer; var q, r: Integer);