假设有以下设置:
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
最佳答案
可能是最新版本的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;
关于ada - **Post** 合约中的 `' Old` 属性如何处理可能在函数或过程中被解除分配的访问类型?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/69554224/