Operational semantics

Operational semantics is 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 meaning of a program in the strict language is explained in terms of a hypothetical computerwhich performs the set of actions which constitute the elaboration of that program. (Algol68, Section 2)It is all very well to aim for a more ‘abstract’ and a ‘cleaner’ approach tosemantics, but if the plan is to be any good, the operational aspects cannotbe completely ignored. (Scott70) Operational semantics is 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 terminatingsequence 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.) Perhaps the first formal incarnation of operational semantics was the use of the lambda calculus to define the semantics of LISP. Abstract machines in the tradition of the SECD machine are also closely related. 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 first use of the term 'operational semantics' in its present meaning is attributed toDana Scott (Plotkin04).What follows is a quote from Scott's seminal paper on formal semantics,in which he mentions the 'operational' aspects of semantics. Gordon Plotkin introduced the structural operational semantics, Robert Hieb and Matthias Felleisen the reduction contexts, and Gilles Kahn the natural 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. 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 {displaystyle C_{1},C_{2}} range over programs of the language, and let s {displaystyle s} range over states (e.g. functions from memory locations to values). If we have expressions (ranged over by E {displaystyle E} ), values ( V {displaystyle V} ) and locations ( L {displaystyle L} ), then a memory update command would have semantics: ⟨ E , s ⟩ ⇒ V ⟨ L := E , s ⟩ ⟶ ( s ⊎ ( L ↦ V ) ) {displaystyle {frac {langle E,s angle Rightarrow V}{langle L:=E,,,s angle longrightarrow (suplus (Lmapsto V))}}}