ada - Ada spark - --# 派生句を追加

Question

私はこの手順に派生句を追加しようとしていますが、これが私の解決策です:

--# Key から Index、Data & Found から 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;