Теорія програмування

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

Пример 1.

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

Доказать:

 

Пример 2.

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

Доказать:

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

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

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

 

 

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

var u, v: Real;

begin

     x := a;  y := b;

     Repeat

        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;

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

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

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

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

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

begin

  r := b;

  q := 0;

  While r >= b do begin

    r := r - a;

    q := q + 1

  end                  

  {Invariance equality: a = b*q + r, Invariant: a - b*q - r}     

end;

Таким чином, поліноміальні інваріантні рівності мають вигляд , де . Інваріант, що відповідає цій рівності, має вигляд  .

Ідеали програмних інваріантів. Основні властивості.

Наведемо необхідні алгебраїчні визначення й твердження.