[<-] 在为什么 3 中是什么意思？

【问题标题】：What does [ <- ] mean in why3?[<-] 在为什么 3 中是什么意思？
【发布时间】：2015-07-15 19:18:54
【问题描述】：

我正在使用 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] 是什么意思。

在访问t_1[a_5 <- x]之前是x到a_5的赋值吗？

【问题讨论】：

标签： smt frama-c why3

【解决方案1】：

[ <- ] 是Why3 中数组修改的符号。然而，与命令式语言不同，t[i <- v] 是t 的功能更新，即将i 映射到v 的（新）数组以及@987654327 的所有其他有效索引@ 到它们在t 中的值。 t 本身是未修改的，您正在通过复制 t 的大部分内容来创建一个新数组。

这些是Why3 standard library on arrays的相关部分

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

【讨论】：