GNATprove: «проверка переполнения может завершиться ошибкой» в функции возведения в степень - PullRequest
Новая
       34

GNATprove: «проверка переполнения может завершиться ошибкой» в функции возведения в степень

0 голосов
/ 24 октября 2018

Я не могу решить эту проблему с SPARK 2018, думаю, мне нужен какой-то инвариант для решения проблемы переполнения, но я уже все перепробовал и не могу его найти.Если бы кто-то мог пролить свет на мою проблему.

Я попробую Экспонирование в простом режиме и в двоичном режиме путем последовательного возведения в квадрат.

Заранее большое спасибо.

ЭТО ОШИБКИ: 

practica.adb:20:17: medium: overflow check might fail (e.g. when A = 0 and r = 1)
practica.adb:40:33: medium: loop invariant might fail after first iteration, cannot prove r * (x ** y) = (M ** N (e.g. when M = 0 and N = 0 and r = 0 and x = 0 and y = 0)
practica.adb:44:20: medium: overflow check might fail (e.g. when x = 0)
practica.adb:47:20: medium: overflow check might fail (e.g. when r = 0 and x = 0)
practica.ads:8:19: medium: postcondition might fail, cannot prove power_simple'Result = (A ** B (e.g. when A = 0 and B = 2 and power_simple'Result = 0)
practica.ads:16:22: medium: postcondition might fail, cannot prove power_binary'Result = (M ** N (e.g. when M = 0 and N = 2 and power_binary'Result = 0)

Это мой код .ads 

package Practica with SPARK_Mode => On is

   -- Funcion que calcula la potenciacion de A elevado a B
   function power_simple (A : Natural; B : Natural) return Integer
     with Depends => (power_simple'Result => (A,B)), 
          Pre => B >= 0,
          Post => power_simple'Result = (A ** B)
                  and (if B = 0 then power_simple'Result = 1);


   -- Funcion que calcula mediante exponenciacion binaria, potencias de un numero dado
   function power_binary (M : Integer; N : Integer) return Integer
       with  Depends => (power_binary'Result => (M,N)),
             Pre => (M >= 0) and (N >= 0),
             Post => power_binary'Result = (M ** N)
             and (if N = 0 then power_binary'Result = 1);

end Practica;

и этомой код .adb 

   -- Funcion que calcula la potenciacion de A elevado a B
   function  power_simple (A : Natural; B : Natural) return Integer is
      x : Integer := 0;
      r : Integer := 1;
   begin

      while x /= B loop
         pragma Loop_Invariant (0 <= x);
         pragma Loop_Invariant (x <= B);
         pragma Loop_Invariant (r = (A ** x));
         pragma Loop_Invariant (r >= 0);
         pragma Loop_Invariant ((if x = 0 then r /= 0));
         pragma Loop_Variant (Decreases => B - x);

         r := r * A;
         x := x + 1;

      end loop;

      if (B = 0) then r := 1; end if;
      if (B = 1) then r := A; end if;

      return r;
   end power_simple;


   --Funcion que calcula mediante exponenciacion binaria, potencias de un numero
   function power_binary(M : Integer; N : Integer) return Integer is
      x : Integer := M;
      y : Integer := N;
      r : Integer := 1;
   begin
      while y /= 0 loop
         pragma Loop_Invariant ((x >= 0) and (y >= 0));
         pragma Loop_Invariant (r * (x ** y) = (M ** N));
         pragma Loop_Variant (Decreases => y);

         if (y mod 2) = 0 then
            x := x * x;
            y := y / 2;
         else
            r := r * x;
            y := y - 1;
         end if;
      end loop;

      if (N = 0) then r := 1; end if;
      if (N = 1) then r := M; end if;

      return r;
   end power_binary;
...