Search code examples
smtframa-cwhy3

What does [ <- ] mean in why3?

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]?

Solution

  • [ <- ] 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