We have defined single-assignment in another section as follows:
Once a value (or a new value) has been assigned to a variable then after this assignment this variable stands for this value in this same program branch. This allows us (but does not force us) to view a Lava variable as a logical variable and an assignment as a logical statement which expresses the requirement that its left-hand side should be identical to its right-hand side.
The logical semantics considers Lava statements as logical statements that are to be verified, or rendered true, in a certain order (from top to bottom). Particularly the ";" separator between statements is interpreted as "logical and" conjunction in this view. Formal parameters of functions are free variables, all other variables are quantified by the unbounded logical quantifier declare or by the bounded quantifiers exists, foreach or the by the set constructor select. The logical semantics enables us to revise the transaction notion in a quite satisfactory way.
But you can also continue to apply the traditional imperative semantics and view a Lava variable as a container and an assignment as an instruction to put the value of its right-hand side into the container designated by its left-hand side.
From the imperative point of view Lava statements are instructions that are to be executed and ";" means sequential execution. The declare quantifier is viewed as a traditional declaration statement, the bounded quantifiers exists and foreach are viewed as loop constructs, and select corresponds to the SQL select expression.
Clearly a really precise formal definition of the Lava semantics would require much greater efforts. (For further study.)
See also: