Structural operational semantics Developed by Gordon Plotkin Configurations:  has one of two forms:  S, s  Statement S is about to execute on state s sTerminal (final) state Transitions  S, s     =  S', s'  Execution of S from s is not completed and remaining computation proceeds from intermediate configuration   = s'Execution of S from s has terminated and the final state is s'  S, s  is stuck if there is no  such that  S, s    84 first step