Завершение цикла
Я хочу доказать, что цикл в этой процедуре завершится с помощью варианта (связанная функция)
вариант будет I
и нижняя граница 0
(I: = 0)
на каждом повторении, размер I
будет уменьшаться до достижения нижней границы 0
Как я могу доказать это I
будет уменьшаться в этом цикле?
procedure Find
(Key: Integer;
Data : in MyArray;
Index: out Integer;
Found: out Boolean)
--# post (Found -> Data(Index) = Key);
is
I: Integer;
begin
I := 0;
Found := False;
loop
--# assert (I >= 0) and
--# (I <= Data'Last + 1) and
--# (Found -> Data(I) = Key);
exit when (I > Data 'Last) or Found;
if(Data(I)) = Key
then
Found := True;
else
I:= I + 1;
end if;
end loop;
Index := I;
end Find;
3 ответа
Я не уверен, что вы подразумеваете под "вариантом" и "связанной функцией", и у меня нет доступа к вашей версии SPARK.
В SPARK 2014, с GNAT CE 2018, это доказывает (после большой боли, может быть, мне стоит пройтись по некоторым учебникам SPARK) без каких-либо инвариантов цикла.
Я думаю, что я мог бы уйти без Supported_Range
если я запустил цикл в обратном порядке.
Я бы хотел заменить True
в постусловии с (for all D of Data => D /= Key)
, но я оставлю это на этом.
Я понимаю, что это не отвечает на ваш вопрос, извините.
package Memo with SPARK_Mode is
subtype Supported_Range is Natural range 0 .. Natural'Last - 1;
type My_Array is array (Supported_Range range <>) of Integer;
procedure Find
(Key : Integer;
Data : My_Array;
Index : out Integer;
Found : out Boolean)
with
Pre => Data'Length >= 1,
Post => ((Found and then Index in Data'Range and then Data (Index) = Key)
or else True);
end Memo;
package body Memo with SPARK_Mode is
procedure Find
(Key : Integer;
Data : My_Array;
Index : out Integer;
Found : out Boolean)
is
subtype Possible_J is Integer range Data’Range;
J : Possible_J;
begin
J := Possible_J'First;
Index := -1; -- have to initialize with something
Found := False;
loop
if Data (J) = Key
then
Found := True;
Index := J;
exit;
else
exit when J = Data'Last;
J := J + 1;
end if;
end loop;
end Find;
end Memo;
Если я напишу это в типичной ида идиоме, я получу
package SPARK_Proof is
type Integer_List is array (Positive range <>) of Integer;
type Find_Result (Found : Boolean := False) is record
case Found is
when False =>
null;
when True =>
Index : Positive;
end case;
end record;
function Match_Index (Value : Integer; List : Integer_List) return Find_Result;
end SPARK_Proof;
package body SPARK_Proof is
function Match_Index (Value : Integer; List : Integer_List) return Find_Result is
-- Empty
begin -- Match_Index
Search : for I in List'Range loop
if Value = List (I) then
return (Found => True, Index => I);
end if;
end loop Search;
return (Found => False);
end Match_Index;
end SPARK_Proof;
Это короче и понятнее. Я не знаю, легче ли это доказать с помощью SPARK.
Я бы использовал конструкцию с ограниченным циклом (для цикла) для перебора массива. Цикл for легче обрабатывает границы массивов и пустые массивы. Это работает для меня в GNAT CE 2018 (здесь используется SPARK 2014):
package Foo with SPARK_Mode => On is
type MyArray is array (Integer range <>) of Integer;
procedure Find
(Key : in Integer;
Data : in MyArray;
Index : out Integer;
Found : out Boolean)
with
Post => (if Found then Data (Index) = Key);
end Foo;
а также
package body Foo with SPARK_Mode => On is
----------
-- Find --
----------
procedure Find
(Key : in Integer;
Data : in MyArray;
Index : out Integer;
Found : out Boolean)
is
begin
Found := False;
Index := Data'First;
for I in Data'Range loop
if Data (I) = Key then
Found := True;
Index := I;
end if;
pragma Loop_Invariant
(Index in Data'Range);
pragma Loop_Invariant
(if Found then Data (Index) = Key else Data (Index) /= Key);
exit when Found;
end loop;
end Find;
end Foo;