Formal Semantics
形式语义（formal semantics） 在编程语言语法中为有效字符串分配计算意义，是 形式语言 的一部份。形式语义 描述了计算机执行程序的过程，具体而言就是输入、输出之间的关系，或者程序在特定平台执行的流程。
Wikipedia
In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid strings in a programming language syntax. It is closely related to, and often crosses over with, the semantics of mathematical proofs.
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.[1]