Что означает [<-] в почему?

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] средства.

Это назначение 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