Почему это переполнение в кондор в Аде? - PullRequest
Новая
       13

Почему это переполнение в кондор в Аде?

0 голосов
/ 22 июня 2019

Я не знаю, почему ошибка при переполнении в переменном факторе.Мне нужна помощь. 

 contador: Integer;
   J: Integer;

   function noPrimos (lista : My_Array) return Boolean

   with
      Global  => contador,
      --Depends => ...,
      Pre     => True and contador < Integer'Last,
      Post    => (noPrimos'Result = True or noPrimos'Result = False);  



FILE ADB

function noPrimos (lista : My_Array)  return Boolean is
      contador: Integer;
   begin
      for I in lista'Range loop
         contador:= 0;
         if lista(I) /= 1 then
            for J in 1.. lista(I) loop
               if lista(I) rem J = 0 then
                  contador := contador + 1;
               end if;
            end loop;
            if contador <= 2 then
               return false;
            end if;
         else
            return true;
         end if;
         pragma Loop_Variant(Increases => I);
      end loop;
      return true;
   end noPrimos;

Проблема заключается в переполнении результата: Фаза 1 из 2: генерация глобальных контрактов ... Фаза 2 из 2: анализ и подтверждение потока ... 15:40: среда: проверка переполнения может быть неудачной (например, когда contador = 2147483647) 47:40: среда: проверка переполнения может быть неудачной (например, когда contador = 0)

1 Ответ

3 голосов
/ 23 июня 2019

Прежде всего, я предполагаю, что функция noPrimos вернет True, только если список lista не содержит простых чисел. При этом я немного озадачен некоторыми аспектами фрагмента кода:

  • Определение типа My_Array отсутствует.

  • Роль глобального экземпляра contador (англ .: counter) не ясна из данного фрагмента кода. Написав Global=> contador, вы заявляете, что глобальная переменная contador будет прочитана функцией noPrimos (см. Также здесь ), но этого не происходит, потому что локальный экземпляр contador скрывает глобальный экземпляр contador.

  • Причина, по которой переменная J определяется глобально, не ясна, ее можно опустить.

  • Предварительное условие True (слева от логического оператора and) тривиально и может быть опущено.

  • Постусловие гласит, что результатом noPrimos может быть True или False. Это тривиально, так как noPrimos возвращает логическое значение и поэтому может быть опущено. Постусловие должно указывать ожидаемый результат функции с учетом ее входных данных.

  • Вариант цикла pragma Loop_Variant(Increases => I); тривиален, так как переменная I будет увеличиваться по определению цикла for. Следовательно, вариант цикла может быть опущен.

Ниже приведен пример функции No_Primes, которая ищет в заданном списке L простые числа и возвращает True, если ничего не найдено. Это доказано в GNAT CE 2019:

primes.ads (spec) 

package Primes with SPARK_Mode is

   type List is
     array (Natural range <>) of Positive;

   --
   --  Returns True if N is a prime number (or False otherwise).
   --
   function Is_Prime (N : Positive) return Boolean
     with
       Global => null,
       Post => Is_Prime'Result =
         (if N = 1 then False
            else (for all I in 2 .. N - 1 => N rem I /= 0));  

   --
   -- Returns True if list L does not contain any prime numbers (or False otherwise).
   --
   function No_Primes (L : List) return Boolean
     with
       Global => null,
       Post => No_Primes'Result =
         (for all I in L'Range => Is_Prime (L (I)) = False);

end Primes;

primes.adb (тело) 

package body Primes with SPARK_Mode is

   --------------
   -- Is_Prime --
   --------------

   function Is_Prime (N : Positive) return Boolean is
   begin
      if N = 1 then
         return False;
      else
         for I in 2 .. N - 1 loop

            if N rem I = 0 then               
               return False;
            end if;

            pragma Loop_Invariant
              (for all J in 2 .. I => N rem J /= 0);

         end loop;
      end if;
      return True;
   end Is_Prime;

   ---------------
   -- No_Primes --
   ---------------

   function No_Primes (L : List) return Boolean is
   begin

      for I in L'Range loop

         if Is_Prime (L (I)) then
            return False;
         end if;

         pragma Loop_Invariant
           (for all J in L'First .. I => Is_Prime (L (J)) = False);

      end loop;
      return True;

   end No_Primes;

end Primes;

Небольшая тестовая программа ( main.adb ) 

with Ada.Text_IO; use Ada.Text_IO;
with Primes;      use Primes;

procedure Main is

   --  Some test vectors.
   L1 : List := (1 => 1);         --  Expect TRUE  : 1 is not a prime.
   L2 : List := (1, 2, 3, 5, 7);  --  Expect FALSE : All are prime except 1.
   L3 : List := (2, 3, 5, 7);     --  Expect FALSE : All are prime.
   L4 : List := (1, 4, 6, 8, 9);  --  Expect TRUE  : None are prime.
   L5 : List := (4, 6, 8, 9);     --  Expect TRUE  : None are prime.
   L6 : List := (3, 4, 5);        --  Expect FALSE : 3 and 5 are prime.

begin
   Put_Line ("No_Primes (L1) = " & Boolean'Image (No_Primes (L1)));
   Put_Line ("No_Primes (L2) = " & Boolean'Image (No_Primes (L2)));
   Put_Line ("No_Primes (L3) = " & Boolean'Image (No_Primes (L3)));
   Put_Line ("No_Primes (L4) = " & Boolean'Image (No_Primes (L4)));
   Put_Line ("No_Primes (L5) = " & Boolean'Image (No_Primes (L5)));
   Put_Line ("No_Primes (L6) = " & Boolean'Image (No_Primes (L6)));
end Main;

выходы 

No_Primes (L1) = TRUE
No_Primes (L2) = FALSE
No_Primes (L3) = FALSE
No_Primes (L4) = TRUE
No_Primes (L5) = TRUE
No_Primes (L6) = FALSE
...