У меня есть функция, которая должна возвращать количество найденных островов.
Я назвал эту функцию Count_Islands, которая принимает параметр Map_Array типа Map, где Map представляет собой массив островов.
Острова — тип перечислителя с набором Земля, Вода.
У меня есть спецификация функции в .ads и тело в файле .adb
Проблема, с которой я сталкиваюсь сейчас, заключается в том, как доказать, что моя функция Результат Count_Islands будет меньше (X * Y)
Я пробовал: с сообщением => 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;
Есть ли лучший способ доказать эту арифметику? Спасибо за помощь.
@ Брайан, они связаны. Спасибо за интерес.
Поскольку пример неполный, я позволил себе немного изменить его. Вы можете доказать пост-условие, добавив инварианты цикла. Программа ниже доказывает в 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, я просмотрел свой пример и пришел к выводу, что вам на самом деле не нужны призрачные переменные. Все, что вам нужно, это два инварианта цикла. Смотрите обновленный ответ.
Пример недостаточно полон, чтобы догадаться. Как X и Y связаны с X_Range и Y_Range? Проблема может заключаться в этом или в < vs <=.