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