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


3.2.7 DEFINE declarations

In order to make descriptions more concise, a symbol can be associated with a commonly expression. The syntax for this kind of declaration is:

define_declaration :: "DEFINE"
                    atom ":=" simple_expr ";"
                    atom ":=" simple_expr ";"
                    ...
                    atom ":=" simple_expr ";"

Whenever an identifier referring to the symbol on the left hand side of the `:=' in a DEFINE occurs in an expression, it is replaced by the expression on the right hand side. The expression on the right hand side is always evaluated in its context, however (see section 3.2.9 MODULE declarations for an explanation of contexts). Forward references to defined symbols are allowed, but circular definitions are not allowed, and result in an error.

Defined symbols cannot be given values non-deterministically. Another difference between defined symbols and variables is that while variables are statically typed, definitions are not.



NuSMV <nusmv@irst.itc.it>