P in Program
C in Command
E in Expression
B in Booleanexpr
I in Identifier
P ::= C.
C ::= I := E  C_1; C_2  C1
 C2

if B then C_1
else C_2  while B do C
 Parallel evaluation operator .
 Assignment is noninterruptable.
 Exclusive access to store.
 Interleaving semantics
 Evaluation of C_1C_2 interleaves assignments of
C_1 with those of C_2.
 Semantics of C_1C_2 generates set of results of
all possible interleavings.