For many programming languages, the only formal semantics published is an SOS big-step semantics. Such a semantics is not suited for investigations that observe intermediate states, such as invariant techniques. In this paper, a construction is proposed that generates automatically a small-step SOS semantics from a big-step semantics. This semantics is based on the a priori technique pioneered by Willem-Paul de Roever et al.
|Title of host publication||Concurrency, Compositionality, and Correctness (Essays in honor of Willem-Paul de Roever)|
|Editors||D. Dams, U. Hannemann, M. Steffen|
|Place of Publication||Berlin|
|Number of pages||8|
|Publication status||Published - 2010|
|Name||Lecture Notes in Computer Science|