4

假设具有以下设置：

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西蒙赖特提到的。

编辑：Self允许的固定类型null

4

2 回答 2

3

可能是最新版本的 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;
于 2021-10-13T14:33:38.980 回答
2

在ARM 6.1.1(26ff)中它说

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

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

X'Old : 常数 S := X;

...换句话说，没有什么花哨的，只是（在这种情况下）的直接副本Self: not Self.all。

因此，如果您的Replacedeallocates Self，那么Self’Old是一个悬空引用，并且是错误的。

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

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

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

Self’Old.all注意和之间的细微差别Self.all’Old。第一个获取Self调用之前的副本，在调用之后被取消引用（此时它指向超空间），而第二个取消引用先验Self并复制它在那里找到的整数值；返回时仍然有效。

于 2021-10-15T11:05:45.443 回答