Editing Semantics (computer science) (section)

==Variations==
Some variations of formal semantics include the following:

* '''[[Action semantics]]'''<ref name=Mosses1996>{{cite report |author-link=Peter Mosses|author-first=Peter D.|author-last=Mosses |date=1996 |title=Theory and practice of action semantics |publisher=[[Aarhus University]] |series=BRICS Report RS9653}}</ref> 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 (computer science)|Algebraic semantics]]'''<ref name=Goguen77/> is a form of [[axiomatic semantics]] based on [[algebra]]ic laws for describing and reasoning about [[program semantics]] in a [[formal methods|formal]] manner. It also supports [[denotational semantics]] and [[operational semantics]];
* '''[[Attribute grammar]]s'''<ref>{{cite book |author1-first=Pierre|author1-last=Deransart |author2-first=Martin|author2-last=Jourdan |author3-first=Bernard|author3-last=Lorho |title="Attribute Grammars: Definitions, Systems and Bibliography |date=1988 |series=Lecture Notes in Computer Science 323 |publisher=[[Springer-Verlag]] |isbn=9780387500560}}</ref> define systems that systematically compute "[[metadata]]" (called ''attributes'') for the various cases of [[Syntax (programming languages)|the language's 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 [[compiler]]s, and to augment [[Regular languages|regular]] or [[Context-free languages|context-free grammars]] with [[Context-sensitive languages|context-sensitive]] conditions;
* '''[[Categorical semantics|Categorical]] (or "functorial") semantics'''<ref name=Lawvere1963>{{cite journal |author-link=William Lawvere|author-first=F. William|author-last=Lawvere |title=Functorial semantics of algebraic theories |journal=[[Proceedings of the National Academy of Sciences of the United States of America]] |volume=50 |issue=5 |date=1963 |pages=869–872 |doi=10.1073/pnas.50.5.869|pmid=16591125 |pmc=221940 |bibcode=1963PNAS...50..869L |doi-access=free }}</ref> uses [[category theory]] as the core mathematical formalism. 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;<ref>{{cite journal |author1=Andrzej Tarlecki |author2=[[Rod Burstall|Rod M. Burstall]] |author3=[[Joseph Goguen|Joseph A. Goguen]] |title=Some fundamental algebraic tools for the semantics of computation: Part 3. Indexed categories |journal=[[Theoretical Computer Science]] |volume=91 |issue=2 |date=1991 |pages=239–264 |doi=10.1016/0304-3975(91)90085-G|doi-access=free }}</ref>
* '''[[Concurrency semantics]]'''<ref>{{cite conference |author1-first=Mark|author1-last=Batty |author2-first=Kayvan|author2-last=Memarian |author3-first=Kyndylan|author3-last=Nienhuis |author4-first=Jean|author4-last=Pichon-Pharabod |author5-first=Peter|author5-last=Sewell |title=The problem of programming language concurrency semantics |book-title=Proceedings of the European Symposium on Programming Languages and Systems |pages=283–307 |publisher=[[Springer Publishing|Springer]] |date=2015 |doi=10.1007/978-3-662-46669-8_12|doi-access=free |url=http://kar.kent.ac.uk/50271/1/c_concurrency_challenges.pdf }}</ref> is a catch-all term for any formal semantics that describes concurrent computations.  Historically important concurrent formalisms have included the [[actor model]] and [[process calculi]];
* '''[[Game semantics]]'''<ref name=Abramsky2009>{{cite book |author-link=Samson Abramsky|author-first=Samson|author-last=Abramsky |chapter=Semantics of interaction: An introduction to game semantics |title=Semantics and Logics of Computation |date=2009 |pages=1–32 |doi=10.1017/CBO9780511526619.002  |publisher=Cambridge University Press |isbn=9780521580571 |url=https://ora.ox.ac.uk/objects/uuid:ab3ece5b-cd8d-49e6-ba33-010ea4c1a1ac |editor1=Andrew M. Pitts |editor2=P. Dybjer}}</ref> uses a metaphor inspired by [[game theory]];
* '''[[Predicate transformer semantics]]''',<ref name=Dijkstra1975>{{cite journal |author-link=Edsger W. Dijkstra|author-first=Edsger W.|author-last=Dijkstra |date=1975 |title=Guarded commands, nondeterminacy and formal derivation of programs |journal=[[Communications of the ACM]] |volume=18 |issue=8 |pages=453–457 |doi=10.1145/360933.360975|s2cid=1679242 |doi-access=free }}</ref> 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.