我正在使用 Frama-C、Alt-Ergo 和 Why3 进行系统验证。在 Frama-C 中生成并发送到 Why3 的一项证明义务如下所示(这是 Why3 版本):
(p_StableRemove t_1[a_5 <- x] a_1 x_1 a i_2)
我想知道什么t_1[a_5 <- x]
意思。
访问之前是x
to的分配吗?a_5
t_1[a_5 <- x]
[ <- ]
是Why3 中数组修改的符号。但是,与命令式语言不同,t[i <- v]
它是 的功能更新,t
即映射i
到的(新)数组v
,以及 的所有其他有效索引t
到它们在 中的值t
。t
本身是未修改的,您正在通过复制大部分内容来创建一个新数组t
。
这些是关于数组的Why3标准库的相关部分
function set (a: array ~'a) (i: int) (v: 'a) : array 'a =
{ a with elts = M.set a.elts i v }
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v