11 lines
382 B
Ada
11 lines
382 B
Ada
procedure Find_First
|
|
(List : in Array_Type;
|
|
Value : in Integer;
|
|
Found : out Boolean;
|
|
Position : out Positive) with
|
|
Depends => ((Found, Position) => (List, Value)),
|
|
Pre => (List'Length > 0),
|
|
Post =>
|
|
(if Found then Position in List'Range and then List (Position) = Value
|
|
else Position = List'Last);
|