1. Given the following formal specification, write the TSL specification for Search.
procedure Search (Key : ELEM ; T: SEQ of ELEM;
Found : BOOLEAN; L: ELEM_INDEX) ;
Pre-condition
-- the sequence has at least one element
T'FIRST <= T'LAST
Post-condition
-- the element is found and is referenced by L
( Found and T (L) = Key)
or
-- the element is not in the array
( not Found and
not (exists i, T'FIRST <= i <= T'LAST, T (i) = Key ))