'''Operational semantics''' areis a category of [[Semantics (computer science)|formal programming language semantics]] in which certain desired properties of a program, such as correctness, safety or security, are [[formal verification|verified]] by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms ([[denotational semantics]]). Operational semantics are classified in two categories: '''structural operational semantics''' (or '''small-step semantics''') formally describe how the ''individual steps'' of a [[computation]] take place in a computer-based system. By opposition '''natural semantics''' (or '''big-step semantics''') describe how the ''overall results'' of the executions are obtained. Other approaches to providing a [[formal semantics of programming languages]] include [[axiomatic semantics]] and [[denotational semantics]].
The operational semantics for a programming language describes how a valid program is interpreted as sequences of computational steps.
