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 x
to 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 oft
, i.e. a (new) array that mapsi
tov
, and all other valid indexes oft
to their value int
.t
itself is unmodified, you are creating a new array by copying most of the contents oft
.These are the relevant part of the Why3 standard library on arrays