|
|
|---|
|
|
|
|---|
Leo locations.
During execution, Leo reads and writes values in variables. These values may be primitive or aggregate: the latter consist of parts that can be individually read and written; these parts may in turn have sub-parts, recursively.
These individually readable and writable parts are locations. A location may be a variable, or a component of a tuple location, or a component of a struct location; this notion will be extended as more kinds of aggregate values (besides tuples and structs) are added to Leo, most likely arrays. That is, a location consists of a variable (always the starting point) followed by zero or more ``sub-part selectors''. The term `location' is appropriate because these are abstract memory locations.
As a point of comparison, the Java Language Specification uses the term `variable' to denote what we call `locations' here; in Java, a variable is not just a named variable, e.g. it may be an array component. In our Leo formalization, we reserve the term `variable' for the named locations at the top level.