ada - Ada spark - 添加 --# 派生子句

Question

我正在尝试在此过程中添加派生子句，这是我的解决方案：

--# 从 Key 中导出 Index，从 Data 中导出 Data & I 从 Data 中导出；

我不确定，我需要帮助

procedure Find
   (Key: Integer ;
    Data : in MyArray ;
    Index : out Integer ;
    Found : out Boolean )
    --# post (Found -> Data(Index) = Key);
    --# derives ???
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;