中文摘要：

计算机语言的形式语义学是计算机科学的重要研究内容之一,它包括：公理语义、操作语义、指称语义及代数语义。常见的公理语义是通过Hoare三元组构造逻辑系统,使得一个Hoare三元组是正确的当且仅当它可以从该逻辑系统推出;操作语义是从迁移系统的角度研究程序的逐步行为;指称语义是指用相应的数学对象（如,集合,函数等等）对语言的语义进行注释,其基础是论域理论及λ-演算;代数语义是用代数方法对语言的语义进行注释,其基础包括范畴论、抽象数据类型的说明与实现等。另外,最弱前置条件语义及最弱线性条件语义也是一种公理语义。它们转化后置条件为最弱（线性）前置条件。这两者的区别是前者对应全正确的程序（是指程序一定终止）;而后者对应部分正确的程序（是指程序不一定终止）。

英文摘要：

Formal semantics is one of research contents of computer science, which includes axiomatic, operational, denotational and algebraic semantics. General axiomatic semantics constructs a logical systems in virtue of Hoare triple such that a Hoare triple is correct if and only if it can be deduced from this logical system; the operational semantics studies the stepwise behaviour of a program from the point of transitionsystems; the denotational semantics remarks the semantics of a language by the corresponding mathematical objects （for example, set, function and so on）, whose foundations are domain theory and 2-calculus; the algebraic semantics remarks the semantics of a language by the algebraic methods, whose foundations include category theory, the explanation and realization of abstract data types and so on. In addition, the weakest （liberal） precondition semantics are also axiomatic semantics. They both transform the postcondition to the corresponding weakest （liberal） precondition. The difference between them is. the former deals with total correctness programs （i. e. , the program must terminate）, while the latter deals with partial correctness programs （i. e. , the program need not terminate）.