对于可能在函数或过程中被释放的访问类型，在**Post**合同中的`'Old`‘属性是如何处理的？
假设具有以下设置：
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合同中的使用将变得无效，您如何仍然可以访问以前的值？是否可以在预契约中创建手动快照，然后在Post中使用？也许可以用Ghost_Code来实现？
我想在星火里制造一切，以防有什么改变。
编辑：将Self修正为in out，正如Simon所提到的。
编辑：固定类型的允许null的Self
回答 2
Stack Overflow用户
发布于 2021-10-15 11:05:45
在ARM 6.1.1(26 ARM)中，它说
启用后条件表达式中的每个X‘’Old表示在子程序体、条目体或接受语句的开头隐式声明的常量。 以X‘’Old的每次出现所表示的隐式声明实体声明如下： X‘’Old:常数S := X；
..。换句话说，不需要任何花哨的东西，只是Self：而不是Self.all的一个直接副本。
因此，如果您的Replace释放Self，那么Self’Old是一个悬空引用，并且是错误的。
我之前建议将postcondition更改为
Post => Self.all'Old /= Self.all;是安全的，为什么不能满足你的要求呢？有什么事你没跟我们说过吗？
注意Self’Old.all和Self.all’Old之间的细微差别。第一个是调用前的Self副本，在调用后被取消引用(此时它指向超空间)，而第二个则退出先前的Self并复制它在那里找到的整数值；返回时，这个值仍然有效。
Stack Overflow用户
发布于 2021-10-13 14:33:38
可能是最新版本的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;https://stackoverflow.com/questions/69554224
复制相似问题
腾讯云开发者
