4 lines
73 B
Text
4 lines
73 B
Text
|
procedure P (X : in out Integer);
|
||
|
|
--# derives X from *;
|
||
|
|
--# post X = 42;
|