ada - 如何在 ada 后置条件中为函数参数分配新值

Question

我一直在尝试很多事情并寻找解决方案，但我找不到。

我被卡住了，因为我需要为 ada 函数中的后置条件分配一个新值

例如，使用以下函数：

function Square(A: in out INTEGER) return INTEGER
   with 
      Pre => A > 0,
      Post => Square'Result = A * A
....

我想知道如何例如增加参数 A 或将其设置为后置条件内的随机值，如 42

谢谢