Как выполнять арифметические операции контракта с функцией, принимающей тип 2D-массива в качестве параметра в Аде

  1. У меня есть функция, которая должна возвращать количество найденных островов.

  2. Я назвал эту функцию Count_Islands, которая принимает параметр Map_Array типа Map, где Map представляет собой массив островов.

  3. Острова — тип перечислителя с набором Земля, Вода.

  4. У меня есть спецификация функции в .ads и тело в файле .adb

  5. Проблема, с которой я сталкиваюсь сейчас, заключается в том, как доказать, что моя функция Результат Count_Islands будет меньше (X * Y)

  6. Я пробовал: с сообщением => Count_Islands'Result < X * Y -- Всякий раз, когда я пытался доказать все, что у меня есть: среда: постусловие может ошибка не может доказать Count_Islands'Result < X * Y

Функция в .ads:

function Count_Islands(Map_Array : Map) 
    return Integer with Pre => Map_Array'Length /= 0, 
                        Post => Count_Islands'Result < X * Y;

Функция в .adb:

function Count_Islands(Map_Array : Map) return Integer
   is
      Visited_Array : Visited := (others => (others=> False));
      Count : Integer := 0;
   begin
      if (Map_Array'Length = 0)then
         return 0;
      end if;
      for i in X_Range loop
         for j in Y_Range loop
            if (Map_Array(i, j) = Land and then not Visited_Array(i,j)) then
               Visited_Array := Visit_Islands(Map_Array, i, j,Visited_Array);
               Count := Count + 1;
            end if;
         end loop;
      end loop;
      return Count;
   end Count_Islands;

Например, в матрице 4 * 5 то есть мой X = 4 и Y = 5:

Я ожидаю, что выходной результат острова (земли) будет равен 1, что меньше 4 * 5. Но GNATprove не может доказать, что мой первоначальный код анализирует это, используя Post => Count_Islands'Result < X * Y;

Есть ли лучший способ доказать эту арифметику? Спасибо за помощь.

Пример недостаточно полон, чтобы догадаться. Как X и Y связаны с X_Range и Y_Range? Проблема может заключаться в этом или в < vs <=.

user_1818839 26.07.2019 17:28

@ Брайан, они связаны. Спасибо за интерес.

Simple_tech 27.07.2019 23:16
Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
1
2
123
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Поскольку пример неполный, я позволил себе немного изменить его. Вы можете доказать пост-условие, добавив инварианты цикла. Программа ниже доказывает в GNAT CE 2019:

main.adb

procedure Main with SPARK_Mode is

   --  Limit the range of the array indices in order to prevent 
   --  problems with overflow, i.e.:
   --
   --     Pos'Last * Pos'Last <= Natural'Last
   --
   --  Hence, as Natural'Last = 2**31 - 1,
   --
   --     Pos'Last <= Sqrt (2**31 - 1) =approx. 46340
   --
   --  If Pos'Last >= 46341, then overflow problems might occur. 

   subtype Pos is Positive range 1 .. 46340;

   type Map_Item is (Water, Land);

   type Map is
     array (Pos range <>, Pos range <>) of Map_Item;

   type Visited is
     array (Pos range <>, Pos range <>) of Boolean;


   function Count_Islands (Map_Array : Map) return Natural with
     Post => Count_Islands'Result <= Map_Array'Length (1) * Map_Array'Length (2);


   -------------------
   -- Count_Islands --
   -------------------

   function Count_Islands (Map_Array : Map) return Natural is

      Visited_Array : Visited (Map_Array'Range (1), Map_Array'Range (2)) :=
        (others => (others => False));

      Count : Natural := 0;

   begin

      for I in Map_Array'Range (1) loop

         pragma Loop_Invariant
           (Count <= (I - Map_Array'First (1)) * Map_Array'Length (2));

         for J in Map_Array'Range (2) loop            

            pragma Loop_Invariant
              (Count - Count'Loop_Entry <= J - Map_Array'First (2));

            if Map_Array(I, J) = Land and then not Visited_Array(I, J) then
               Visited_Array (I, J) := True;   --  Simplified
               Count := Count + 1;
            end if;

         end loop;

      end loop;      

      return Count;

   end Count_Islands;

begin
   null;
end Main;

@AspMVCAda, я просмотрел свой пример и пришел к выводу, что вам на самом деле не нужны призрачные переменные. Все, что вам нужно, это два инварианта цикла. Смотрите обновленный ответ.

DeeDee 11.07.2019 20:24

Другие вопросы по теме