公理语义(axiomatic semantics) 运用数学中的公理化方法给出的计算机语言的语义。 不同的人在了解程序的含义时有不同的要求。例如，有的人只关心程序的数据输入和输出，而不关心程序是否正确终止。公理语义就是研究如何将这些不同的要求形式化，并根据这些要求严格给出程序设计语言的语义。
1967年美国R．W．Floyd提出描述人们所关心的程序含义，以及如何去论证一个程序是否具有某种含义的数学方法，1969年英国C．A．R．Hoare首次用公理系统定义了一类程序设计语言的语义。1975年荷兰E．W．Dijkstra提出基于最弱前置条件的公理语义描述方法。 在定义语言的公理语义时，必须先给出描述所关心的程序语义的形式化方法，然后建立公理系统，规定语言成分的有关语义。如果用一个程序户去计算自然数的阶乘，这个程序中的变量x在程序开始执行时，存放用户输入的自然数值k；而在程序执行终止时，存放要输出的结果。用户关心的是程序户计算的结果值是否确是输入值的阶乘。在公理语义中，使用公式A表示程序P的这一部分含义；若P执行前x的值等于k，则P执行完毕后x的值等于A(k) 。程序p执行前的条件称为P的前置条件，执行后的条件称为P的后置条件。这类公式称为归纳命题；若程序P执行前，其程序变量的值满足前置条件R，则程序P执行完毕后，其程序变量的值满足后置条件Q。归纳命题用来作为描述程序语义的工具，公理语义就是用归纳命题的公理系统来定义程序语言的语义。
- 其他语言成分的公理语义也是用公理和推理规则类似地给出，但有的成分(如过程调用等)的语义，比起上述语句的语义要复杂得多。
论证一个程序是否具有某种含义的过程和论证一个程序是否具有某种特性的过程是完全一致的。故公理语义学是程序正确性研究的理论基础。程序验证的研究也进一步促进公理语义学的发展。 寻求适用于描述程序语义，且便于语义推导的逻辑语言是公理语义学研究的一个重要方面。 20世纪70年代出现了使用时态逻辑来定义语言的语义，称为时态语义。另外如动态逻辑、算法逻辑在语义学中的应用，也都在发展之中。
(李晓山 周巢尘)
