Unified semantic language: syntax, semantics, and pragmatics

A new language of finite state machines called USL is proposed. The language is intended for rapid development of formal verification-oriented operational semantics of modern programming languages. Formal operational semantics of the USL language is defined. The USL-based approach to programming language semantics design is illustrated by the example of a definition of С# jump statements.