Ada/SPARK中Post契约'Old属性对内部释放访问类型的处理问题

问题1：释放内存后访问Self'Old.all会出现什么问题？ #

会触发未定义行为：

• Self'Old只会存过程调用前Self指针本身的地址值，不会保存地址指向的堆数据
• 调用Unchecked_Deallocation后该地址对应的堆内存已经被释放，属于无效内存
• Post契约中解引用Self'Old.all就是悬空指针访问，轻则读到垃圾值导致契约校验逻辑错误，重则直接触发段错误导致程序崩溃

问题2：Ada是否会自动生成Self'Old的堆内存快照？ #

不会。Ada标准明确规定Old属性仅保存对象本身的值，对于访问类型（指针）来说，仅保存指针存储的地址值，不会做深度拷贝。你需要自己手动实现原值的保存。

问题3：如何在Post阶段访问原先的值？能否用Ghost代码实现？ #

完全可以，推荐用Ghost变量实现手动快照，不会影响正式业务代码的运行，示例实现如下：

with Ada.Unchecked_Deallocation;

procedure Replace(Self : in out My_Acc; New_Int : Integer)
  with
    Pre => Self /= null and then New_Int /= Self.all, -- 补充判空适配允许null的类型约束
    Post => Self /= null and then Old_Val /= Self.all
is
    -- Ghost变量仅用于验证，不会编译进最终发布的二进制
    Old_Val : My with Ghost;
    procedure Free is new Ada.Unchecked_Deallocation(My, My_Acc);
begin
    -- 释放内存前先把原值存到Ghost变量
    Old_Val := Self.all;
    Free(Self);
    Self := new My'(New_Int);
end Replace;

你不需要在Pre契约里做特殊处理，只要在过程最开始、内存释放前完成Ghost变量的赋值即可，Post契约可以直接读取这个Ghost变量的值。

问题4：SPARK约束会对方案产生影响吗？ #

SPARK不仅不会影响方案，反而会强化正确性：

1. 如果你直接在Post契约里写Self'Old.all，SPARK证明器会直接报错，提示你访问了可能失效的内存，提前把问题扼杀在编译验证阶段
2. 上述Ghost变量的实现方案是SPARK原生支持的特性，只要你确保在释放内存前完成对Ghost变量的赋值，SPARK可以完全证明Post契约的正确性
3. SPARK对Unchecked_Deallocation的使用有严格的合法性校验，该方案符合SPARK的内存安全要求

内容的提问来源于stack exchange，提问作者mhatzl