有没有会spark ada的想请问几道题。

Question

如果 I 和 J 在堆栈的当前大小范围内，该过程将只交换值； 否则，堆栈不变。
procedure Swap(I, J: in Pointer_Range)
with
通过添加 Global、Depends、Pre、Post 或 Contract_Cases 方面来完成规范，以指定过程的预期行为。