Go to the first, previous, next, last section, table of contents.

3.2.3 ASSIGN declarations

An assignment has the form:

assign_declaration :: "ASSIGN"
           assign_body ";"
           assign_body ";"
           ...

assign_body ::
           atom                ":=" simple_expr     ;; normal assignment
         | "init" "(" atom ")" ":=" simple_expr     ;; init assignment
         | "next" "(" atom ")" ":=" next_expr       ;; next assignment

On the left hand side of the assignment, atom denotes the current value of a variable, `init(atom)' denotes its initial value, and `next(atom)' denotes its value in the next state. If the expression on the right hand side evaluates to an integer or symbolic constant, the assignment simply means that the left hand side is equal to the right hand side. On the other hand, if the expression evaluates to a set, then the assignment means that the left hand side is contained in that set. It is an error if the value of the expression is not contained in the range of the variable on the left hand side.

In order for a program to be implementable, there must be some order in which the assignments can be executed such that no variable is assigned after its value is referenced. This is not the case if there is a circular dependency among the assignments in any given process. Hence, such a condition is an error. In it is an error for a variable to be assigned a value more than once at any given time. More precisely, it is an error if:

1. the next or current value of a variable is assigned more than once in a given process, or
2. the initial value of a variable is assigned more than once in the program, or
3. the current value and the initial value of a variable are both assigned in the program, or
4. the current value and the next value of a variable are both assigned in the program.