A Model of Program Execution

Formalize operational view of program execution.

• Set of (infinite) execution sequences.
  • Sequence $R$, $i$-th element $R$_i.
  • $R$_i = ($R$_i.state, $R$_i.label).
  • $R$_i.label denotes statement selected for execution in $i$-th step.
  • $R$_i.state is program state (values of program variables) before $i$-th step.
• Sequence construction:
  • Initial state $R$₀.state (need not be the same for all sequences).
  • $R$_i.state and $R$_i.label determine $R$_i+1.state.
  • $R$₀.label and $R$_j.state (for all ) determine $R$_i.state.