形式语义学
维基百科，自由的百科全书
在计算理论中, 形式语义学是关注计算的模式和程序设计语言的含义的严格的数学研究的领域。
语言的形式语义是用数学模型去表达该语言描述的可能的计算来给出的。
提供程序设计语言的形式语义的方法很多，其中主要类别有：
- 指称语义学，着重于语言的执行结果而非过程，包括域理论；
- 操作语义学，例如抽象机（象SECD machine），着重于描述语言的过程；
- 公理语义学，如 谓词变换语义学和代数语义学。
其他方法还有：
一些非中文的文字因为尚未翻譯而被隐藏，歡迎參與翻譯。
- Action semantics, which is a kind of hybrid of denotational and operational semantics;
- Attribute grammars, used also for augmenting regular or context-free grammars with context-sensitive conditions, and for code generation;
- Categorical semantics (also called Functorial semantics), which is most easily understood as an algebraic semantics (and so is an axiomatic semantics), but which can also be understood as a kind of denotational semantics, and indeed familiarity with category theory is today a requirement for understanding most work in denotational semantics;
- Concurrency semantics, for example based on the Actor model and process calculi;
- Game semantics was proposed as a kind of denotational semantics, but it has a dynamical aspect that allows it to be understood as a kind of operational semantics.
Different formal semantics may be linked through abstractions within the theory of abstract interpretation.
The field of formal semantics also studies the relations between different models, the relations between different approaches to meaning, and 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.
