Блог

Главная - Вопросы по программированию - Как доказать этот инвариант?

Как доказать этот инвариант?

#ada #proof #invariants #proof-of-correctness #spark-ada

Вопрос:

Я стремлюсь доказать, что правило Хорнера верно. Для этого я сравниваю значение, вычисляемое в настоящее время Хорнером, со значением «реального» полинома.
Поэтому я создал этот фрагмент кода:

 package body Poly with SPARK_Mode is
   function Horner (X : Integer; A : Vector) return Integer is
      Y : Integer := 0;
      Z : Integer := 0 with Ghost;
   begin
      for I in reverse A'First .. A'Last loop
         pragma Loop_Invariant (Y * (X ** (I - A'First   1)) = Z);
         Y := A(I)   Y * X;
         Z := Z   A(I) * (X ** (I - A'First));
      end loop;
      pragma Assert (Y = Z);
      return Y;
   end Horner;
end Poly;

Что должно доказать инвариантность. К сожалению, gnatprove говорит мне:

 cannot prove  Y * (X ** (I - A'First   1)) = Z
e.g. when A = (1 => 0, others => 0) and A'First = 0 and A'Last = 1 and I = 0 and X = 1 and Y = -1 and Z = 0

Как это работает, что Y=-1 в этом случае? У вас есть какие-нибудь идеи, как это исправить?

Комментарии:

1. я бы не стал слишком концентрироваться на контрпримере здесь. Вполне вероятно, что это не доказано из-за использования здесь силы. Это действительно тяжелая операция для проверяющего. Хорошим началом было бы разделить базу и показатель. Например, вы должны доказать, что X ** V у этого есть верхняя граница, которая включает в себя отображение верхней границы для X и V = I - A'First 1 отдельно. Хотя это все еще может быть трудно для испытателя.

Ответ №1:

контрпример здесь является ложным, он не соответствует реальному недопустимому выполнению. Арифметика слишком сложна для проверки, что приводит как к тому, что сохранение инварианта цикла не доказано, так и к ложному контрпримеру.

Чтобы исследовать такую недоказанную проверку, вы должны войти в «автоматически активный» режим проверки свойств, который требует разбиения свойства на более мелкие, пока либо автоматические проверяющие не смогут справиться с меньшими шагами, либо вы можете изолировать недоказанное элементарное свойство, которое вы можете изолировать в лемме, которую вы можете проверить отдельно.

Здесь я ввел призрачную переменную YY для значения Y в начале итерации и разбил инвариант цикла на все меньшие и меньшие утверждения, которые показали, что проблема заключалась в возведении в степень (X ** (I — A’First 1) = X * (X ** (I — A’First)), которое я также выделил в утверждении:

 package body Poly with SPARK_Mode is
   function Horner (X : Integer; A : Vector) return Integer is
      Y : Integer := 0;
      Z : Integer := 0 with Ghost;
      YY : Integer with Ghost;
   begin
      for I in reverse A'First .. A'Last loop
         pragma Loop_Invariant (Y * (X ** (I - A'First   1)) = Z);
         YY := Y;
         Y := A(I)   Y * X;
         Z := Z   A(I) * (X ** (I - A'First));
         pragma Assert (Z = YY * (X ** (I - A'First   1))   A(I) * (X ** (I - A'First)));
         pragma Assert (X ** (I - A'First   1) = X * (X ** (I - A'First)));
         pragma Assert (Z = YY * X * (X ** (I - A'First))   A(I) * (X ** (I - A'First)));
         pragma Assert (Z = (YY * X   A(I)) * (X ** (I - A'First)));
         pragma Assert (Z = Y * (X ** (I - A'First)));
      end loop;
      pragma Assert (Y = Z);
      return Y;
   end Horner;
end Poly;

Теперь все утверждения и инвариант цикла доказываются с помощью —level=2 с помощью SPARK Community 2020. Конечно, некоторые утверждения не нужны, поэтому вы можете их удалить.

Метки: