Operational semantics: Difference between revisions

Revision as of 04:10, 19 January 2021

Revision as of 10:31, 4 March 2021

Line 1:

{{Semantics}}'''Operational semantics''' is a category of [[SemanticsFormal (computer science)language|formal programming language]] [[Semantics (computer science)|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. 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.)

These sequences then ''are'' the meaning of the program.

In the context of [[functional program]]s, 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.)

Perhaps the first formal incarnation of operational semantics was the use of the [[lambda calculus]] to define the semantics of [[LISPLisp (programming language)|Lisp]].<ref>{{Cite web| |title=Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I |last=McCarthy author|first=John McCarthy| author-link=John McCarthy (computer scientist)| |url=http://www-formal.stanford.edu/jmc/recursive.html| |access-date=2006-10-13| |url-status=dead| |archive-url=https://web.archive.org/web/20131004215327/http://www-formal.stanford.edu/jmc/recursive.html| |archive-date=2013-10-04}}</ref> [[Abstract machine]]s in the tradition of the [[SECD machine]] are also closely related.

== History ==

Line 31 ⟶ 27:

== Approaches ==

[[Gordon Plotkin]] introduced the structural operational semantics, Robert Hieb and [[Matthias Felleisen]] the reduction contexts,<ref>{{cite journal |title=The Revised Report on the Syntactic Theories of Sequential Control and State | journal=Theoretical Computer Science | last1=Felleisen | first1=M. | last2=Hieb | first2=R. | year=1992 | volume=103 | issue=2 | pages=235–271 | doi = 10.1016/0304-3975(92)90014-7 }}</ref> and [[Gilles Kahn]] the natural semantics.

=== Small-step semantics ===

==== Structural operational semantics ====

'''Structural operational semantics''' (SOS, also called '''structured operational semantics''' or '''small-step semantics''') was introduced by [[Gordon Plotkin]] in ([[#plotkin81|Plotkin81]]) as a logical means to define operational semantics. The basic idea behind SOS is to define the behavior of a program in terms of the behavior of its parts, thus providing a structural, i.e., syntax-oriented and [[inductive definition|inductive]], view on operational semantics. An SOS specification defines the behavior of a program in terms of a (set of) [[State transition system|transition relation]](s). SOS specifications take the form of a set of [[inference rule]]s that define the valid transitions of a composite piece of syntax in terms of the transitions of its components.

For a simple example, we consider part of the semantics of a simple programming language; proper illustrations are given in [[#plotkin81|Plotkin81]] and [[#hennessybook|Hennessy90]], and other textbooks. Let <math>C_1, C_2</math> range over programs of the language, and let <math>s</math> range over states (e.g. functions from memory locations to values). If we have expressions (ranged over by <math>E</math>), values {{nobreak|(<math>V</math>)}} and locations (<math>L</math>), then a memory update command would have semantics:

Line 143 ⟶ 139:

*<cite id=plotkin04> [[Gordon Plotkin|Gordon D. Plotkin.]] The Origins of Structural Operational Semantics. J. Log. Algebr. Program. 60-61:3-15, 2004. ([http://homepages.inf.ed.ac.uk/gdp/publications/Origins_SOS.pdf preprint]). </cite>

*<cite id=scott70> [[Dana Scott|Dana S. Scott.]] Outline of a Mathematical Theory of Computation, Programming Research Group, Technical Monograph PRG–2, Oxford University, 1970.</cite>

*<cite id=algol68> [[Adriaan van Wijngaarden]] et al. [[ALGOL 68|Revised Report on the Algorithmic Language [[ALGOL 68]]. IFIP. 1968.]] ([http://vestein.arb-phys.uni-dortmund.de/~wb/RR/rr.pdf]{{dead link|date=March 2018 |bot=InternetArchiveBot |fix-attempted=yes }})</cite>

*<cite id=hennessybook>[[Matthew Hennessy]]. Semantics of Programming Languages. Wiley, 1990. [https://www.cs.tcd.ie/matthew.hennessy/splexternal2015/resources/sembookWiley.pdf available online].</cite>