I'm using Frama-C, Alt-Ergo and Why3 for system verifications. One proof obligation generated in Frama-C and sent to Why3 is shown below (this is the Why3 version):
(p_StableRemove t_1[a_5 <- x] a_1 x_1 a i_2)
I'd like to know what t_1[a_5 <- x] means.
Is it an assignment of xto a_5 before accessing t_1[a_5 <- x]?
[ <- ] is the notation for array modification in Why3. However, unlike in imperative languages, t[i <- v] is a functional update of t, i.e. a (new) array that maps i to v, and all other valid indexes of t to their value in t. t itself is unmodified, you are creating a new array by copying most of the contents of t.
These are the relevant part of the 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