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

Question

我使用Frama、Alt和Why3进行系统验证.在Frama中生成并发送给Why3的一个证明义务如下所示(这是Why3版本)：

(p_StableRemove t_1[a_5 <- x] a_1 x_1 a i_2)

我想知道t_1[a_5 <- x]是什么意思。

这是在访问x之前将a_5分配给t_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