Reference no: EM131715849

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 ))