2.4.3 Variables

If id is an identifier, T a non-empty type other than an open array type, and E an expression, then:

    VAR id: T := E
declares id as a variable of type T whose initial value is the value of E. Either ``:= E'' or ``: T'' can be omitted, but not both. If T is omitted, it is taken to be the type of E. If E is omitted, the initial value is an arbitrary value of type T. If both are present, E must be assignable to T.

The initial value is a shorthand that is equivalent to inserting the assignment id := E at the beginning of the executable part of the block. If several variables have initial values, their assignments are inserted in the order they are declared. For example:

    VAR i: [0..5] := j; j: [0..5] := i; BEGIN S END
initializes i and j to the same arbitrary value in [0..5]; it is equivalent to:
    VAR i: [0..5]; j: [0..5]; BEGIN i := j; j := i; S END

If a sequence of identifiers share the same type and initial value, id can be a list of identifiers separated by commas. Such a list is shorthand for a list in which the type and initial value are repeated for each identifier. That is:

    VAR v_1, ..., v_n: T := E
is shorthand for:
    VAR v_1: T := E; ...; VAR v_n: T := E
This means that E is evaluated n times.

m3-support@elego.de