Home > Articles > Programming > General Programming/Other Languages

  • Print
  • + Share This
This chapter is from the book

Assignments And Expressions

As in C, the assignments

c = c + 1; c = c - 1 /* valid */

can be abbreviated to

c++; c--             /* valid */

but, unlike in C,

b = c++

is not a valid assignment in PROMELA, because the right-hand side operand is not a side effect free expression. There is no equivalent to the shorthands

--c; ++c            /* not valid */

in PROMELA, because assignment statements such as

c = c-1; c = c+1    /* valid */

when taken as a unit are not equivalent to expressions in PROMELA. With these constraints, a statement such as --c is always indistinguishable from c--, which is supported.

In assignments such as

variable = expression

the values of all operands used in the expression on the right-hand side of the assignment operator are first cast to signed integers, before any of the operands are applied. The operator precedence rules from C determine the order of evaluation, as reproduced in Table 3.2. After the evaluation of the right-hand side expression completes, and before the assignment takes place, the value produced is cast to the type of the target variable. If the right-hand side yields a value outside the range of the target type, truncation of the assigned value can result. In simulation mode SPIN issues a warning when this occurs; in verification mode, however, this type of truncation is not intercepted.

It is also possible to use C-style conditional expressions in any context where expressions are allowed. The syntax, however, is slightly different from the one used in C. Where in C one would write

expr1 ? expr2 : expr3       /* not valid */

one writes in PROMELA

(expr1 -> expr2 : expr3)    /* valid */

The arrow symbol is used here to avoid possible confusion with the question mark from PROMELA receive operations. The value of the conditional expression is equal to the value of expr2 if and only if expr1 evaluates to true and otherwise it equals the value of expr3. PROMELA conditional expressions must be surrounded by parentheses (round braces) to avoid misinterpretation of the arrow as a statement separator.

Table 3.2. Operator Precedence, High to Low




() [] .

left to right

parentheses, array brackets

! ~ ++ --

right to left

negation, complement, increment, decrement

* / %

left to right

multiplication, division, modulo

+ -

left to right

addition, subtraction

<< >>

left to right

left and right shift

< <= > >=

left to right

relational operators

== !=

left to right

equal, unequal


left to right

bitwise and


left to right

bitwise exclusive or


left to right

bitwise or


left to right

logical and


left to right

logical or

-> :

right to left

conditional expression operators


right to left

assignment (lowest precedence)

  • + Share This
  • 🔖 Save To Your Account