package Loop_Invariant1 is type Arr is array (Natural range <>) of Integer; procedure Proc (A : Arr; N : Integer); end Loop_Invariant1;