Operational semantics 270062 224557295 2008-07-09T11:56:18Z Smrmousavi 7439260 /* References */ In [[computer science]], '''operational semantics''' is a way to give meaning to [[computer program]]s in a mathematically rigorous way (See [[formal semantics of programming languages]]). 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 program]]s, the final step in a terminating sequence returns the value of the program. (In general there can be many computation sequences and many return values for a single program, because the program could be [[Nondeterminism|nondeterministic]].) For the first time, the concept of operational semantics was used in defining the semantics of Algol 68. The following statement is a quote from the revised ALGOL 68 report: <blockquote> 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|Algol68]], Section 2) </blockquote> The first use of the word "operational semantics" in its present meaning is attributed to Dana Scott ([[#plotkin04b|Plotkin04b]]). What follows is a quote from Scott's seminal paper on formal semantics, in which he mentions the "operational" aspects of semantics. <blockquote> 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|Scott70]]) </blockquote> Perhaps the first formal incarnation of operational semantics was that of the [[lambda calculus]]. Abstract machines in the tradition of the [[SECD machine]] are also closely related. == Structural Operational Semantics (SOS) == Structural Operational Semantics (SOS) was introduced by Gordon Plotkin in ([[#plotkin04a|Plotkin04a]]) as a logical means to defining 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 which define the valid transitions of a composite piece of syntax in terms of the transitions of its components. Such a definition allows formal analysis of the behavior of programs, permitting the study of [[Relation (mathematics)|relations]] between programs. Important relations include [[simulation preorder]]s and [[bisimulation]]. These are especially useful in the context of [[Concurrency (computer science)|concurrency theory]]. 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 ([[#plotkin04a|Plotkin04a]]) has attracted some 900 citations according to the CiteSeer [http://citeseer.ist.psu.edu/673965.html], making it one of the most cited technical reports in [[Computer Science]]. == See also == * [[Algebraic semantics]] * [[Axiomatic semantics]] * [[Denotational semantics]] * [[Formal semantics of programming languages]] == References == * <cite id=plotkin04a> [[Gordon Plotkin | Gordon D. Plotkin.]] [http://citeseer.ist.psu.edu/673965.html 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) ([http://homepages.inf.ed.ac.uk/gdp/publications/sos_jlap.pdf preprint]). </cite> * <cite id=plotkin04b> [[Gordon Plotkin | Gordon D. Plotkin.]] The Origins of Structural Operational Semantics. JALP. 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 | 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])</cite> [[Category:Formal specification languages]] [[Category:Logic in computer science]] [[Category:Semantics]] [[de:Operationale Semantik]] [[fr:Sémantique opérationnelle]] [[hr:Operacijska semantika]] [[ja:操作的意味論]] [[pt:Semântica operacional]]