| author | wenzelm |
| Mon, 13 Apr 2020 22:08:14 +0200 | |
| changeset 71751 | abf3e80bd815 |
| parent 45044 | 2fae15f8984d |
| permissions | -rw-r--r-- |
| 45044 | 1 |
package Loop_Invariant |
2 |
is |
|
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 |
||
14 |
end Loop_Invariant; |