按要求添加 Global、Depends、Pre、Post 或 Contract_Cases

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

k

下面是完整的规范：

with Global =>
(Size > 0 and then (I >= 1 and I <= Size and J >= 1 and J <= Size)),
Depends => Current_Size,
Pre =>
(Current_Size > 0 and then (I >= 1 and I <= Current_Size and J >= 1 and J <= Current_Size)),
Post =>
(if Size > 0 and Current_Size > 0 and I >= 1 and I <= Size and J >= 1 and J <= Size then
(Elements(I) = Old(Elements(J)) and Elements(J) = Old(Elements(I)))
else
unchanged Elements),
Contract_Cases => (I, J);

该规范指定了一些过程的行为。

Global 方面指定了过程中使用的一些全局规定，即 I 和 J 必须在堆栈的大小范围内，否则过程无效。
Depends 方面指定了过程的行为取决于堆栈的当前大小。
Pre 方面指定了过程的前置条件，即堆栈必须包含至少一个元素，并且 I 和 J 必须在堆栈的当前大小范围内。
Post 方面指定了过程执行后的预期行为。如果堆栈包含至少一个元素并且 I 和 J 在堆栈的大小范围内，则交换了 I 和 J 对应的元素；否则，堆栈不变。
Contract_Cases 方面指定了过程的合同情况，即 I 和 J。