**Post** 合同中的“旧”属性如何处理可能在函数或过程中释放的访问类型？
How is the `'Old` attribute in a **Post** contract handled for access types that might got deallocated inside the function or procedure?
假设具有以下设置：
type My is new Integer;
type My_Acc is access My;
procedure Replace(Self : in out My_Acc; New_Int : Integer)
with Pre => New_Int /= Self.all, Post => Self'Old.all /= Self.all;
注意：上面的代码可能不完全有效，但我希望这个概念是可以理解的。
现在如果 Unchecked_Deallocation() 用于 Self 内部 Replace 会发生什么
并分配一个新的 Integer 并将其设置为 Self（这应该导致 Self'Old 指向现在无效的内存位置）?
Ada 是否保留某种快照，其中 Self'Old 指向先前的内存位置，但在执行 Unchecked_Deallocation() 之前？
如果 Self'Old 在 Post 合同中使用无效，你怎么还能访问以前的值？是否可以在 Pre 合约中创建一个手动快照，然后在 Post 中使用？也许可以使用 Ghost_Code?
来实现
我想在 Spark 中制作所有内容，以防发生变化。
编辑： 将 Self 固定为 in out，如 Simon Wright 所述。
编辑： Self 的固定类型允许 null
可能是最新版本的SPARK支持访问类型；以前根本不会。
首先，您的 Not_Null_My_Acc 需要是 My_Acc 的子类型，除非您希望它本身就是一个类型。
其次，你不能在 Replace 中释放 Self 并分配一个新值； Self 处于模式中，因此不可写。
第三，不能将’Old应用到Self，因为
warning: attribute "Old" applied to constant has no effect
你能说的是
Post => Self.all'Old /= Self.all;
Each X'Old in a postcondition expression that is enabled denotes a constant that is implicitly declared at the beginning of the subprogram body, entry body, or accept statement.
The implicitly declared entity denoted by each occurrence of X'Old is declared as follows:
...
X'Old : constant S := X;
...换句话说，没有什么特别的，只是（在这种情况下）Self 的直接复制：not Self.all。
因此，如果您的 Replace 取消分配 Self，那么 Self’Old 是一个悬空引用，并且是错误的。
我之前建议将后置条件更改为
Post => Self.all'Old /= Self.all;
会很安全；为什么不能满足您的要求？有什么事你没告诉我们吗？
请注意 Self’Old.all 和 Self.all’Old 之间的细微差别。第一个获取调用前 Self 的副本，在调用后取消引用（此时它指向超空间），而第二个取消引用先前的 Self 并复制它在那里找到的整数值；在 return 上仍然有效。
假设具有以下设置：
type My is new Integer;
type My_Acc is access My;
procedure Replace(Self : in out My_Acc; New_Int : Integer)
with Pre => New_Int /= Self.all, Post => Self'Old.all /= Self.all;
注意：上面的代码可能不完全有效，但我希望这个概念是可以理解的。
现在如果 Unchecked_Deallocation() 用于 Self 内部 Replace 会发生什么
并分配一个新的 Integer 并将其设置为 Self（这应该导致 Self'Old 指向现在无效的内存位置）?
Ada 是否保留某种快照，其中 Self'Old 指向先前的内存位置，但在执行 Unchecked_Deallocation() 之前？
如果 Self'Old 在 Post 合同中使用无效，你怎么还能访问以前的值？是否可以在 Pre 合约中创建一个手动快照，然后在 Post 中使用？也许可以使用 Ghost_Code?
我想在 Spark 中制作所有内容，以防发生变化。
编辑： 将 Self 固定为 in out，如 Simon Wright 所述。
编辑： Self 的固定类型允许 null
可能是最新版本的SPARK支持访问类型；以前根本不会。
首先，您的 Not_Null_My_Acc 需要是 My_Acc 的子类型，除非您希望它本身就是一个类型。
其次，你不能在 Replace 中释放 Self 并分配一个新值； Self 处于模式中，因此不可写。
第三，不能将’Old应用到Self，因为
warning: attribute "Old" applied to constant has no effect
你能说的是
Post => Self.all'Old /= Self.all;
Each X'Old in a postcondition expression that is enabled denotes a constant that is implicitly declared at the beginning of the subprogram body, entry body, or accept statement.
The implicitly declared entity denoted by each occurrence of X'Old is declared as follows: ...
X'Old : constant S := X;
...换句话说，没有什么特别的，只是（在这种情况下）Self 的直接复制：not Self.all。
因此，如果您的 Replace 取消分配 Self，那么 Self’Old 是一个悬空引用，并且是错误的。
我之前建议将后置条件更改为
Post => Self.all'Old /= Self.all;
会很安全；为什么不能满足您的要求？有什么事你没告诉我们吗？
请注意 Self’Old.all 和 Self.all’Old 之间的细微差别。第一个获取调用前 Self 的副本，在调用后取消引用（此时它指向超空间），而第二个取消引用先前的 Self 并复制它在那里找到的整数值；在 return 上仍然有效。