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

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]是什么意思。

是否在访问t_1[a_5 <- x]之前将x赋值给a_5？

Answer 1

[ <- ]是Why3中数组修改的写法。但是，与命令式语言不同，t[i <- v] 是 t 的 功能更新 ，即映射 i 到 [=15 的（新）数组=]，以及 t 的所有其他有效索引到它们在 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

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

What does [ <- ] mean in why3?

smt

frama-c

why3