Ada spark - Добавить - # Производное предложение

Question

Я пытаюсь добавить пункт производных к этой процедуре, и это мое решение:

- # получает индекс из ключа, данных и находит из данных, а I из данных;

Я не уверен в этом, и мне нужна помощь

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;