1package Loop_Invariant
2is
3
4   type Word32 is mod 2 ** 32;
5
6   procedure Proc1 (A : in Natural; B : in Word32; C : out Word32);
7   --# derives C from A, B;
8   --# post Word32 (A) * B = C;
9
10   procedure Proc2 (A : in Natural; B : in Word32; C : out Word32);
11   --# derives C from A, B;
12   --# post Word32 (A) * B = C;
13
14end Loop_Invariant;
15