author | wenzelm |
Wed, 04 Oct 2017 12:00:53 +0200 | |
changeset 66787 | 64b47495676d |
parent 45044 | 2fae15f8984d |
permissions | -rw-r--r-- |
package body Loop_Invariant is procedure Proc1 (A : in Natural; B : in Word32; C : out Word32) is begin C := 0; for I in Natural range 1 .. A --# assert Word32 (I - 1) * B = C; loop C := C + B; end loop; end Proc1; procedure Proc2 (A : in Natural; B : in Word32; C : out Word32) is begin C := 0; for I in Natural range 1 .. A --# assert Word32 (I - 1) * B = C; loop C := C + B; --# assert Word32 (I) * B = C; end loop; end Proc2; end Loop_Invariant;