对于可能在函数或过程内释放的访问类型，如何处理 **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

，如西蒙·赖特（Simon Wright）所述。

编辑： 修复了

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;

Answer 2

在 ARM 6.1.1(26ff) 它说

启用的后置条件表达式中的每个 X'Old 表示在子程序体、条目体或接受语句的开头隐式声明的常量。

每次出现 X'Old 所表示的隐式声明实体声明如下： ...

X'旧：常数 S := X;

...换句话说，没有什么奇特的东西，只是（在这种情况下）

Self

的直接副本：不是

Self.all

。

因此，如果您的

Replace

释放了

Self

，那么

Self’Old

就是一个悬空引用，并且是错误的。

我之前建议将后置条件更改为

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

会很安全；为什么这不能满足您的要求？有什么事情你没有告诉我们吗？

---

请注意

Self’Old.all

和

Self.all’Old

之间的细微差别。第一个获取

Self

的副本，就像调用之前一样，在调用后取消引用（此时它指向超空间），而第二个则取消引用先前的

Self

并复制它找到的整数值那里;退货后仍然有效。