Content deleted Content added
Korektysta (talk | contribs) m →Reduction semantics: v comes from ‘value’, it's not ν |
Add link to denotational semantics |
||
Line 2:
{{Semantics}}
'''Operational semantics''' is a category of [[Formal language|formal programming language]] [[Semantics (computer science)|semantics]] in which certain desired properties of a [[Computer program|program]], such as correctness, safety or security, are [[formal verification|verified]] by constructing [[Mathematical proof|proof]]s from logical statements about its [[Execution (computing)|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. These sequences then ''are'' the meaning of the program. In the context of [[functional programming]], 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 [[Nondeterministic algorithm|nondeterministic]], 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.)
| |||