Read-only clauses/functions/invariants

Preliminary remark

In Lava, conditional clauses, like if-conditions, are not Boolean or other expressions but quite normal statements, whose evaluation yields a truth value (true or false). This is a consequence of our general opinion that Lava programs are not sequences of instructions/operations but logical statements, and program execution means verification of those statements.

In this context, assignment of values to variables (using the set or copy statements or output parameters of functions) requires particular consideration:

Verification of the statement

set x <== <expression>

simply means to assume the validity of the equation

x = <expression>

for the further verification process. Furthermore, Lava statements have to be ordered in such a way as to enable a sequential verification process. In particular, a value must be assigned (using set/copy or through output parameters) to a variable before it can in turn be used as an input parameter or as part of an expression.

Definition:

An executable Lava construct has the read-only property (or is free of side-effects) if its execution doesn't change any pre-existing objects, i.e., objects that existed already before the execution of the construct started.

Read-only Lava functions

If a function is declared "read-only" then Lava makes sure

  1. that its body assigns values (using set/copy statements, or output parameters) only to declare variables and to output parameters. The body of a read-only initializer may also assign values to attributes of the self object (but not in turn to attributes of attributes, etc.),
  2. that it calls only read-only functions.

These two conditions together guarantee that the function doesn't change any object that existed already before the function call.

Lava constructs with inherent read-only semantics

A Lava construct has inherent read-only semantics if it is

  1. an if, elsif, ifx branching condition, or
  2. a statement that is evaluated by the "?" operator to yield a Boolean true/false result,
  3. a selection condition, i.e., as the where clause of the exists or foreach quantifiers or of the select expression,
  4. an invariant ( = continuation condition) in a class or implementation declaration,
  5. the logical negation not or the exclusive "or" xor , where "A xor B" is interpreted as "((not A) and B) or (A and (not B))".

In contrast to the body of a read-only function, these inherently read-only constructs must not contain declare or any form of assignment for simplicity.

In the first four cases it would be technically possible to allow assignments within these constructs, but it would be problematic to allow them, since a branching/selection/continuation decision could be invalidated by the very evaluation of the controlling conditional, selection, or invariant clause if we would allow side-effects. I.e., the decisive condition for branching, selection, or continuation possibly wouldn't hold any longer immediately after the evaluation.

In case 5 it would have unpleasant technical consequences for the implementation if an assignment would occur in such a clause of the program that would force us to verify the negation of an assignment:

not (x = <expression>)

during the verification process, since x could then assume infinitely many possible values generally (viz. all values not equal to the value of <expression>). Therefore, since we do not like to test the truth value of the program statement for each of these infinitely many possible values of x, we prefer to exclude all constructs from the Lava language that could provoke such a situation.

See also

Logical semantics of Lava