1package body Loop_Invariant 2is 3 4 procedure Proc1 (A : in Natural; B : in Word32; C : out Word32) 5 is 6 begin 7 C := 0; 8 for I in Natural range 1 .. A 9 --# assert Word32 (I - 1) * B = C; 10 loop 11 C := C + B; 12 end loop; 13 end Proc1; 14 15 procedure Proc2 (A : in Natural; B : in Word32; C : out Word32) 16 is 17 begin 18 C := 0; 19 for I in Natural range 1 .. A 20 --# assert Word32 (I - 1) * B = C; 21 loop 22 C := C + B; 23 --# assert Word32 (I) * B = C; 24 end loop; 25 end Proc2; 26 27end Loop_Invariant; 28