World Library  
Flag as Inappropriate
Email this Article

Operational semantics

Article Id: WHEBN0000270062
Reproduction Date:

Title: Operational semantics  
Author: World Heritage Encyclopedia
Language: English
Subject: Semantics, Gordon Plotkin, Denotational semantics, Bisimulation, Operational semantics
Collection: Formal Specification Languages, Logic in Computer Science, Operational Semantics, Programming Language Semantics
Publisher: World Heritage Encyclopedia

Operational semantics

Operational semantics are a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are 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 programs, 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, 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.)

The concept of operational semantics was used for the first time in defining the semantics of Algol 68. The following statement is a quote from the revised ALGOL 68 report:

The meaning of a program in the strict language is explained in terms of a hypothetical computer which performs the set of actions which constitute the elaboration of that program. (Algol68, Section 2)

The first use of the term "operational semantics" in its present meaning is attributed to Dana Scott (Plotkin04). What follows is a quote from Scott's seminal paper on formal semantics, in which he mentions the "operational" aspects of semantics.

It is all very well to aim for a more ‘abstract’ and a ‘cleaner’ approach to semantics, but if the plan is to be any good, the operational aspects cannot be completely ignored. (Scott70)

Perhaps the first formal incarnation of operational semantics was the use of the

  • Gilles Kahn. "Natural Semantics". Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science. Springer-Verlag. London. 1987.
  • Gordon D. Plotkin. A Structural Approach to Operational Semantics. (1981) Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark. (Reprinted with corrections in J. Log. Algebr. Program. 60-61: 17-139 (2004), preprint).
  • Gordon D. Plotkin. The Origins of Structural Operational Semantics. J. Log. Algebr. Program. 60-61:3-15, 2004. (preprint).
  • Dana S. Scott. Outline of a Mathematical Theory of Computation, Programming Research Group, Technical Monograph PRG–2, Oxford University, 1970.
  • Adriaan van Wijngaarden et al. Revised Report on the Algorithmic Language ALGOL 68. IFIP. 1968. ([2])
  • Matthew Hennessy. Semantics of Programming Languages. Wiley, 1990. available online.
  1. ^ Felleisen, M.; Hieb, R. "The Revised Report on the Syntactic Theories of Sequential Control and State". Theoretical Computer Science.  
  2. ^ Abadi, M.; Cardelli, L. A Theory of Objects. 
  3. ^ a b c Xavier Leroy. "Coinductive big-step operational semantics".


See also

Small-step semantics give more control of the details and order of evaluation. In the case of instrumented operational semantics, this allows the operational semantics to track and the semanticist to state and prove more accurate theorems about the run-time behaviour of the language. These properties make small-step semantics more convenient when proving type soundness of a type system against an operational semantics.[3]

The main disadvantage of big-step semantics is that non-terminating (diverging) computations do not have an inference tree, making it impossible to state and prove properties about such computations.[3]

Big-step semantics have the advantage of often being simpler (needing fewer inference rules) and often directly correspond to an efficient implementation of an interpreter for the language (hence Kahn calling them "natural".) Both can lead to simpler proofs, for example when proving the preservation of correctness under some program transformation.[3]

There are a number of distinctions between small-step and big-step semantics that influence whether one or the other forms a more suitable basis for specifying the semantics of a programming language.


Natural semantics (or big-step semantics) ...

Natural semantics

Big-step semantics

The technique is useful for the ease in which reduction contexts can model state or control constructs (e.g., continuations). In addition, reduction semantics have been used to model object-oriented languages,[2] contract systems, and other language features.

This single axiom is the beta rule from the lambda calculus. The reduction contexts show how this rule composes with more complicated terms. In particular, this rule can trigger for the argument position of an application like ((\lambda x.x \; \lambda x.x) \lambda x.(x\;x)) because there is a context ([\,]\; \lambda x.(x\;x)) that matches the term. In this case, the contexts uniquely decompose terms so that only one reduction is possible at any given step. Extending the axiom to match the reduction contexts gives the compatible closure. Taking the reflexive, transitive closure of this relation gives the reduction relation for this language.

(\lambda x.e\; v) \longrightarrow e\,\left[x / v\right] \quad (\mathrm{\beta})

The contexts C include a hole \left[\,\right] where a term can be plugged in. The shape of the contexts indicate where reduction can occur (i.e., a term can be plugged into) a term. To describe a semantics for this language, axioms or reduction rules are provided:

e = v \;|\; (e\; e) \;|\; x \quad\quad v = \lambda x.e \quad\quad C = \left[\,\right] \;|\; (C\; e) \;|\; (v\; C)

Reduction semantics are an alternative presentation of operational semantics using so-called reduction contexts. The method was introduced by Robert Hieb and Matthias Felleisen in 1992 as a technique for formalizing an equational theory for control and state. For example, the grammar of a simple call-by-value lambda calculus and its contexts can be given as:

Reduction semantics

Thanks to its intuitive look and easy to follow structure, SOS has gained great popularity and has become a de facto standard in defining operational semantics. As a sign of success, the original report (so-called Aarhus report) on SOS (Plotkin81) has attracted more than 1000 citations according to the CiteSeer [1], making it one of the most cited technical reports in Computer Science.

Such a definition allows formal analysis of the behavior of programs, permitting the study of relations between programs. Important relations include simulation preorders and bisimulation. These are especially useful in the context of concurrency theory.

If we also have Boolean expressions over the state, ranged over by B, then we can define the semantics of the while command: \frac{\langle B,s\rangle \Rightarrow \mathbf{true}}{\langle\mathbf{while}\ B\ \mathbf{ do }\ C,s\rangle\longrightarrow \langle C;\mathbf{while}\ B\ \mathbf{do}\ C,s\rangle} \quad \frac{\langle B,s\rangle \Rightarrow \mathbf{false}}{\langle\mathbf{while}\ B\ \mathbf{ do }\ C,s\rangle\longrightarrow s}

Informally, the first rule says that, if program C_1 in state s finishes in state s', then the program C_1;C_2 in state s will reduce to the program C_2 in state s'. (You can think of this as formalizing "You can run C_1, and then run C_2 using the resulting memory store.) The second rule says that if the program C_1 in state s can reduce to the program C_1' with state s', then the program C_1;C_2 in state s will reduce to the program C_1';C_2 in state s'. (You can think of this as formalizing the principle for an optimizing compiler: "You are allowed to transform C_1 as if it were stand-alone, even if it is just the first part of a program.") The semantics is structural, because the meaning of the sequential program C_1;C_2, is defined by the meaning of C_1 and the meaning of C_2.

\frac{\langle C_1,s\rangle \longrightarrow s'} {\langle C_1;C_2 \,,s\rangle\longrightarrow \langle C_2, s'\rangle} \quad\quad \frac{\langle C_1,s\rangle \longrightarrow \langle C_1',s'\rangle} {\langle C_1;C_2 \,,s\rangle\longrightarrow \langle C_1';C_2\,, s'\rangle} \quad\quad \frac{} {\langle \mathbf{skip} ,s\rangle\longrightarrow s}

The semantics of sequencing can be given by the following three rules:

Informally, the rule says that "if the expression E in state s reduces to value V, then the program L:=E will update the state s with the assignment L=V".

\frac{\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle\longrightarrow (s\uplus (L\mapsto V))}

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

Structural operational semantics (also called structured operational semantics or small-step semantics) was introduced by Gordon Plotkin in (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, view on operational semantics. An SOS specification defines the behavior of a program in terms of a (set of) transition relation(s). SOS specifications take the form of a set of inference rules that define the valid transitions of a composite piece of syntax in terms of the transitions of its components.

Structural operational semantics

Small-step semantics

Gordon Plotkin introduced the structural operational semantics, Robert Hieb and Matthias Felleisen the reduction contexts,[1] and Gilles Kahn the natural semantics.



  • Approaches 1
    • Small-step semantics 1.1
      • Structural operational semantics 1.1.1
      • Reduction semantics 1.1.2
    • Big-step semantics 1.2
      • Natural semantics 1.2.1
  • Comparison 2
  • See also 3
  • References 4

are also closely related. SECD machine in the tradition of the Abstract machines].  

This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.

Copyright © World Library Foundation. All rights reserved. eBooks from World eBook Library are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.