ada - **Post** 合约中的 `' Old` 属性如何处理可能在函数或过程中被解除分配的访问类型？

Question

假设有以下设置:

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并且分配了一个新的整数并设置为 Self (这应该导致 Self'Old 指向一个现在无效的内存位置)？
Ada 是否在 Self'Old 处保留某种快照？指向前一个内存位置，但在 Unchecked_Deallocation() 之前被执行？
如 Self'Old会在 Post 合约中使用无效，你怎么还能访问以前的值？是否可以在 Pre 合约中创建一个手动快照，然后可以在 Post 中使用？也许可以使用 Ghost_Code 来实现？
我想在 Spark 中制作所有内容，以防发生变化。
编辑:已修复 Self至 in out正如西蒙·赖特所提到的。
编辑: Self固定型允许 null

Answer 1

可能是最新版本的SPARK支持访问类型；它过去根本不会。
首先，您的 Not_Null_My_Acc需要是 My_Acc 的子类型, 除非你的意思是它本身就是一种类型。
其次，你不能释放 Self内Replace并分配一个新值； Self处于模式中，因此不可写。
三、不能申请’Old至 Self ， 因为

warning: attribute "Old" applied to constant has no effect

你能说的是

Post => Self.all'Old /= Self.all;