I have a language for sensor networks (generates C code) and I want to define the formal semantics of it.
The language has this form:
{STATE name_state:
EVERY time
SELECT {variable [, variable] ...}
[SENDIF send_condition]
[CHANGEIF change_condition GOTO new_state];
} ...
START IN initial_state;
- The initial state of the program is specified by the START IN instruction.
- Each state is defined by the STATE instruction.
- In the specification of each state the clauses EVERY and SELECT are compulsory and the clauses SENDIF and CHANGEIF are optional.
- The CHANGEIF clause is only not specified when there is a single state.
What type of formal semantics is more convenient to use?