Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Operational semantics
open-in-new
<p>Operational semantics is a category of <a href="/facts/Formal_language/crDTyP8q">formal programming language</a> <a href="/facts/Semantics_(computer_science)/JEP1zyBv">semantics</a> in which certain desired properties of a <a href="/facts/Computer_program/e38jH9N9">program</a>, such as correctness, safety or security, are <a href="/facts/Formal_verification/BYD4GnJR">verified</a> by constructing <a href="/facts/Mathematical_proof/7ECDrU80">proofs</a> from logical statements about its <a href="/facts/Execution_(computing)/1fyfGMFm">execution</a> and procedures, rather than by attaching mathematical meanings to its terms (<a href="/facts/Denotational_semantics/yRs3ygRA">denotational semantics</a>). Operational semantics are classified in two categories: structural operational semantics (or small-step semantics) formally describe how the <i>individual steps</i> of a <a href="/facts/Computation/qLsELosq">computation</a> take place in a computer-based system; by opposition natural semantics (or big-step semantics) describe how the <i>overall results</i> of the executions are obtained. Other approaches to providing a <a href="/facts/Formal_semantics_of_programming_languages/JEP1zyBv">formal semantics of programming languages</a> include <a href="/facts/Axiomatic_semantics/m7NWmGoV">axiomatic semantics</a> and <a href="/facts/Denotational_semantics/yRs3ygRA">denotational semantics</a>. </p><p>The operational semantics for a <a href="/facts/Programming_language/cWTYbgWa">programming language</a> describes how a valid program is interpreted as sequences of computational steps. These sequences then <i>are</i> the meaning of the program. In the context of <a href="/facts/Functional_programming/cdxqPEIM">functional programming</a>, the final step in a terminating sequence returns the value of the program. (In general there can be many return values for a single program, because the program could be <a href="/facts/Nondeterministic_algorithm/UubLdp3D">nondeterministic</a>, and even for a deterministic program there can be many computation sequences since the semantics may not specify exactly what sequence of operations arrives at that value.) </p><p>Perhaps the first formal incarnation of operational semantics was the use of the <a href="/facts/Lambda_calculus/DaD3RuQ4">lambda calculus</a> to define the semantics of <a href="/facts/Lisp_(programming_language)/xJHA3CrX">Lisp</a>. <a href="/facts/Abstract_machine/zuC4RKLn">Abstract machines</a> in the tradition of the <a href="/facts/SECD_machine/CaJq4ELV">SECD machine</a> are also closely related. </p>