semantics computer science in programming language theory semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages it does so by evaluating the meaning of syntactically valid strings defined by a specific programming language showing the computation involved in such a case that the evaluation would be of syntactically invalid strings the result would be noncomputation semantics describes the processes a computer follows when executing a program in that specific language this can be shown by describing the relationship between the input and output of a program or an explanation of how the program will be executed on a certain platform hence creating a model of computation formal semantics for instance helps to write compilers better understand what a program is doing and to prove eg that the following if statement if 1 1 then s1 else s2 has the same effect as s1 alone overview the field of formal semantics encompasses all of the following the definition of semantic models the relations between different semantic models the relations between different approaches to meaning the relation between computation and the underlying mathematical structures from fields such as logic set theory model theory category theory etc it has close links with other areas of computer science such as programming language design type theory compilers and interpreters program verification and model checking approaches there are many approaches to formal semantics these belong to three major classes denotational semantics whereby each phrase in the language is interpreted as a denotation ie a conceptual meaning that can be thought of abstractly such denotations are often mathematical objects inhabiting a mathematical space but it is not a requirement that they should be so as a practical necessity denotations are described using some form of mathematical notation which can in turn be formalized as a denotational metalanguage for example denotational semantics of functional languages often translate the language into domain theory denotational semantic descriptions can also serve as compositional translations from a programming language into the denotational metalanguage and used as a basis for designing compilers operational semantics whereby the execution of the language is described directly rather than by translation operational semantics loosely corresponds to interpretation although again the implementation language of the interpreter is generally a mathematical formalism operational semantics may define an abstract machine such as the secd machine and give meaning to phrases by describing the transitions they induce on states of the machine alternatively as with the pure lambda calculus operational semantics can be defined via syntactic transformations on phrases of the language itself axiomatic semantics whereby one gives meaning to phrases by describing the logical axioms that apply to them axiomatic semantics makes no distinction between a phrases meaning and the logical formulas that describe it its meaning is exactly what can be proven about it in some logic the canonical example of axiomatic semantics is hoare logic the distinctions between the three broad classes of approaches can sometimes be vague but all known approaches to formal semantics use the above techniques or some combination thereof apart from the choice between denotational operational or axiomatic approaches most variation in formal semantic systems arises from the choice of supporting mathematical formalism variations some variations of formal semantics include the following action semantics is an approach that tries to modularize denotational semantics splitting the formalization process in two layers macro and microsemantics and predefining three semantic entities actions data and yielders to simplify the specification algebraic semantics is a form of axiomatic semantics based on algebraic laws for describing and reasoning about program semantics in a formal manner attribute grammars define systems that systematically compute metadata called attributes for the various cases of the languages syntax attribute grammars can be understood as a denotational semantics where the target language is simply the original language enriched with attribute annotations aside from formal semantics attribute grammars have also been used for code generation in compilers and to augment regular or contextfree grammars with contextsensitive conditions categorical or functorial semantics uses category theory as the core mathematical formalism a categorical semantics is usually proven to correspond to some axiomatic semantics that gives a syntactic presentation of the categorical structures also denotational semantics are often instances of a general categorical semantics concurrency semantics is a catchall term for any formal semantics that describes concurrent computations historically important concurrent formalisms have included the actor model and process calculi game semantics uses a metaphor inspired by game theory predicate transformer semantics developed by edsger w dijkstra describes the meaning of a program fragment as the function transforming a postcondition to the precondition needed to establish it describing relationships for a variety of reasons one might wish to describe the relationships between different formal semantics for example to prove that a particular operational semantics for a language satisfies the logical formulas of an axiomatic semantics for that language such a proof demonstrates that it is sound to reason about a particular operational interpretation strategy using a particular axiomatic proof system to prove that operational semantics over a highlevel machine is related by a simulation with the semantics over a lowlevel machine whereby the lowlevel abstract machine contains more primitive operations than the highlevel abstract machine definition of a given language such a proof demonstrates that the lowlevel machine faithfully implements the highlevel machine it is also possible to relate multiple semantics through abstractions via the theory of abstract interpretation history robert w floyd is credited with founding the field of programming language semantics in floyd 1967 computational semantics formal semantics logic formal semantics linguistics semantic equivalence floyd robert w 1967 assigning meanings to programs pdf in schwartz jt mathematical aspects of computer science proceedings of symposium on applied mathematics 19 american mathematical society pp1932 isbn0821867288 textbooks stump aaron 2014 programming language foundations wiley isbn9781118007471 gunter carl 1992 semantics of programming languages mit press isbn0262071436 harper robert 2006 practical foundations for programming languages pdf archived from the original pdf on 20070627 working draft krishnamurthi shriram 2012 programming languages application and interpretation 2nd ed mitchell john c foundations for programming languages postscript reynolds john c 1998 theories of programming languages cambridge university press isbn0521594146 slonneger kenneth kurtz barry l 1995 formal syntax and semantics of programming languages addisonwesley isbn0201656973 winskel glynn 1993 the formal semantics of programming languages an introduction mit press isbn0262731037 tennent robert d 1991 semantics of programming languages prentice hall isbn9780138055998 hennessy m 1990 the semantics of programming languages an elementary introduction using structural operational semantics wiley isbn9780471927723 nielson h r nielson flemming 1992 semantics with applications a formal introduction pdf wiley isbn9780471929802 nielson h r nielson flemming 2007 semantics with applications an appetizer springer isbn9781846286926 lecture notes winskel glynn denotational semantics pdf university of cambridge aaby anthony 2004 introduction to programming languages archived from the original on 20150619cs1 maint bot originalurl status unknown link semantics 