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

Question

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

访问之前是xto的分配吗？a_5t_1[a_5 <- x]

Answer 1

[ <- ]是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