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