| author | paulson <lp15@cam.ac.uk> |
| Sat, 17 Oct 2020 11:32:03 +0100 | |
| changeset 72492 | 2dd41a8893aa |
| parent 45044 | 2fae15f8984d |
| permissions | -rw-r--r-- |
package Loop_Invariant is type Word32 is mod 2 ** 32; procedure Proc1 (A : in Natural; B : in Word32; C : out Word32); --# derives C from A, B; --# post Word32 (A) * B = C; procedure Proc2 (A : in Natural; B : in Word32; C : out Word32); --# derives C from A, B; --# post Word32 (A) * B = C; end Loop_Invariant;