Lava variables,
stages in the life of a Lava object

Declaration of variables

In addition to literal constants, like "3", a programming language needs "variables" to which you can assign values, like

pi  <==  3.14

In Lava variables may be declared

1. as member variables of classes or implementations using the declaration view of LavaPE,
2. as input or output parameters of functions or initiators using the declaration view of LavaPE,
3. as "unbounded" local variables in execs or invariants using the declare construct in the exec view of LavaPE,
4. as "unbounded" local variables in type ... case branching statements in execs or invariants,
5. as "bounded" local variables ranging over some finite set of objects, using "quantifiers" foreach, exists, select in the exec view of LavaPE,
6. automatically as auxiliary variables "temp..." in the new and clone object creation constructs.

In Lava you have to declare the type (for instance "Integer") and the object category (state or value object) of variables. The type must be either a concrete class or a "virtual type" which has been declared as a "type parameter" of a containing class or package. If the type of a variable is virtual then this virtual type (or one of its ancestors in the inheritance path) may be declared responsible for the determination of the object category.

A tilde "~" precedes the class name in the declaration of state objects and this way indicates that new values may be assigned to their immediate member variables again and again.

Creation, initialization, completion of Lava objects

A concrete object may be created and assigned to acc using the new expression of Lava:

acc <== new ~Account temp
          initialization of the new account:
          temp.accountInit(i1,i2,...)
        but
          customization of the new account:
          temp.balance <== 1000.00;
          ...
        #new

Thereafter acc will point to a newly created state object of type "Account".

Note that new ... #new is an expression in Lava that may occur in any place where expressions are appropriate, not only on the right side of assignments. Therefore it provides an auxiliary variable temp as a reference to the newly created object in the initializer call and in the but customization clause.

Lava demands a more strict separation of the initialization, customization, and usage phases of objects than most other languages. We believe that it is at least worth an experiment to enforce more discipline and to prevent overly chaotic program structures concerning these aspects.

Initialization belongs to the duties of a class provider. Its purpose is to bring a new object into a state where all its non-optional member variables have admissible values such that the methods of the class may be safely applied to the new object.

Customization (in the but clauses of new and clone expressions) gives the class client an opportunity to modify the initialized new object in a client-specific way in cases where the initilizers offered by the class provider do not completely meet the client's requirements.

Here a summary of the pertinent Lava rules:

1. Every Lava class must have at least one "initializer" function (roughly corresponding to a constructor in C++ or Java). You must always specify an initializer (rather than a creatable class) for the new expression.
2. A class may have a "default initializer" without parameters (which will then be omitted from the new expression).
3. Initializers must first call an initializer for every base class of their associated class
4. and must then explicitly assign a value to every non-optional member of the class
5. before they may apply other member functions of their class to their self object.
6. A new object may be passed as a parameter to a function or initiator only after it has left this entire construction hoarding "new ... #new" or "clone ... #clone" and thus counts as complete.
7. Value objects must not be changed any more after completion.

"new <virtual_type>"?: Lava doesn't support the creation of objects whose type is specified as a virtual type. The reason is that a specific initializer is needed on object creation in any case, and initializers are no virtual functions but inseparably associated with a quite specific class. We could at best look for a (parameterless) default initializer (see point 2 above) at run time when the real type is known that corresponds to the specified virtual type. This would represent a kind of virtualization of initializers that we felt to be rather unnatural and arbitrary. Instead, we recommend to resort to the quite usual solution of providing "factory classes" and the usual (virtual) "factory functions" for creating such objects whose real type is only known at run time.

See also object creation.

Lifetime of Lava objects

Roughly speaking, a Lava object may be deleted and the storage allocated to it may be freed when the object is no longer referenced by any Lava variable of any kind: Storage management for Lava objects is based on reference counts.

Persistent objects are realized as persistent component objects in Lava.

Assignment and parameter passing

Assignment of a value (= result of an expression: an object) to a variable means always that the variable is made to point to this object. Parameter passing is viewed as a special case: The value is assigned to a formal input or output parameter of a function or initiator.

Two variables may have the same value, i.e., point to the same object. The reference count of an object is incremented by 1 when the object is assigned to a variable or passed as an input parameter to a function/operator or initiator. It is decremented by 1 if program execution leaves the scope of a variable that points to the object.

See also

Comprehensive initialization checks

Single-assignment

Finalizers/destructors