| dbpprop:abstract
|
- In theoretical computer science, formal semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages and models of computation. The formal semantics of a language is given by a mathematical model that describes the possible computations described by the language. There are many approaches to formal semantics; these approaches belong to three major classes: Denotational semantics, whereby each phrase in the language is translated into a denotation, i.e. a phrase in some other language. Denotational semantics loosely corresponds to compilation, although the "target language" is usually a mathematical formalism rather than another computer language. For example, denotational semantics of functional languages often translates the language into domain theory; 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 phrase's 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 blurry, 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. 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 describes semantics in terms of algebras; Attribute grammars define systems that systematically compute "metadata" (called attributes) for the various cases of 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 compilers, and to augment regular or context-free grammars with context-sensitive conditions; Categorical (or "functorial") semantics uses category theory as the core mathematical formalism; Concurrency semantics 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 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. For a variety of reasons, one might wish to describe the relationships between different formal semantics. For example: One might wish 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. Given a single language, one might define a "high-level" abstract machine and a "low-level" abstract machine for the language, such that the latter contains more primitive operations than the former. One might then wish to prove that an operational semantics over the high-level machine is related by a bisimulation with the semantics over the low-level machine. Such a proof demonstrates that the low-level machine "faithfully implements" the high-level machine. One can sometimes relate multiple semantics through abstractions via the theory of abstract interpretation. 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, 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.
- Formale Semantik beschäftigt sich mit der exakten Bedeutung von künstlichen oder natürlichen Sprachen. Dabei kann sowohl die Bedeutung bestehender Sprachen untersucht als auch die Bedeutung neu geschaffener Sprachen festgelegt werden. In Abgrenzung zur Semantik im allgemeinen Sinn, wie sie vor allem in Philosophie und Linguistik betrieben wird, arbeitet die formale Semantik mit rein formalen, logisch-mathematischen Methoden. Formale Semantik wird in der Logik, in der theoretischen Informatik und in der Linguistik betrieben. Wegen der Wichtigkeit exakter Bedeutungstheorie für die genannten drei Disziplinen und wegen unterschiedlicher Schwerpunkte und Zielsetzungen – teils auch wegen unterschiedlicher Methoden – hat jede dieser Wissenschaften heute ein eigenes Teilgebiet, das als formale Semantik bezeichnet wird. Die formale Semantik aus Logik, jene aus theoretischer Informatik und die formale Semantik aus Linguistik sind jedoch in vielerlei Hinsicht miteinander verflochten und greifen häufig aufeinander bzw. auf die Ergebnisse der jeweils anderen zurück. Die moderne formale Semantik hat ihren Ursprung in Arbeiten von Alfred Tarski, Richard Montague, Alonzo Church und anderen.
- En informatique théorique, la sémantique formelle (des langages de programmation) est l’étude de la signification des programmes informatiques vus en tant qu’objets mathématiques.
- プログラム意味論(Program Semantics)とは、理論計算機科学の一分野で、プログラミング言語の意味と計算モデルに関する厳密な数学的研究領域である。プログラミング言語の形式意味論とも呼ばれる。 ある言語の形式意味論は、その言語で表現可能な処理（計算）を表す数学的モデルによって与えられる。
- Semântica formal é a área de estudo de ciência da computação que se preocupa em especificar o significado (ou comportamento) de programas de computador e partes de hardware. A semântica é complementar à sintaxe de programas de computador, que se preocupa em descrever as estruturas de uma linguagem de programação. A necessidade de uma semântica formal (matemática) para linguagens de programação, justifica-se, pois: Pode revelar ambigüidades na definição da linguagem (o que uma descrição informal não permitiria revelar); É uma base para implementação (síntese), análise e verificação formal.
- Сема́нтика в программировании — система правил определения поведения отдельных языковых конструкций. Семантика определяет смысловое значение предложений алгоритмического языка.
- 在计算理论中, 形式语义学是关注计算的模式和程序设计语言的含义的严格的数学研究的领域。 语言的形式语义是用数学模型去表达该语言描述的可能的计算来给出的。 提供程序设计语言的形式语义的方法很多，其中主要类别有： 指称语义学，着重于语言的执行结果而非过程，包括域理论； 操作语义学，例如抽象机（象SECD抽象机），着重于描述语言的过程； 公理语义学，如 谓词变换语义学和代数语义学。
|
| rdfs:comment
|
- In theoretical computer science, formal semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages and models of computation. The formal semantics of a language is given by a mathematical model that describes the possible computations described by the language.
- Formale Semantik beschäftigt sich mit der exakten Bedeutung von künstlichen oder natürlichen Sprachen. Dabei kann sowohl die Bedeutung bestehender Sprachen untersucht als auch die Bedeutung neu geschaffener Sprachen festgelegt werden. In Abgrenzung zur Semantik im allgemeinen Sinn, wie sie vor allem in Philosophie und Linguistik betrieben wird, arbeitet die formale Semantik mit rein formalen, logisch-mathematischen Methoden.
- En informatique théorique, la sémantique formelle (des langages de programmation) est l’étude de la signification des programmes informatiques vus en tant qu’objets mathématiques.
- プログラム意味論(Program Semantics)とは、理論計算機科学の一分野で、プログラミング言語の意味と計算モデルに関する厳密な数学的研究領域である。プログラミング言語の形式意味論とも呼ばれる。 ある言語の形式意味論は、その言語で表現可能な処理（計算）を表す数学的モデルによって与えられる。
- Semântica formal é a área de estudo de ciência da computação que se preocupa em especificar o significado (ou comportamento) de programas de computador e partes de hardware. A semântica é complementar à sintaxe de programas de computador, que se preocupa em descrever as estruturas de uma linguagem de programação.
- Сема́нтика в программировании — система правил определения поведения отдельных языковых конструкций. Семантика определяет смысловое значение предложений алгоритмического языка.
|
![[RDF Data]](/statics/sw-cube.png)
