什么是公理语义学?

[拼音]：gongli yuyixue

[外文]：axiomatic semantics

形式语义学的一个分支。不同的人在了解程序的含义时有不同的要求。公理语义学方法就是研究如何将这些不同的要求形式化，并根据这些要求严格给出程序设计语言的有关语义。

1967年美国R.W.弗洛依德提出描述人们所关心的程序含义，以及如何去论证一个程序是否具有某种含义的数学方法。1969年英国C.A.R.霍尔首次用公理系统定义了一类程序设计语言的语义。1975年荷兰E.W.戴克斯特拉提出基于最弱前置条件的公理语义学描述方法，成为程序设计方法学的一个基本概念。

在定义语言的公理语义时，必须先给出描述所关心的程序语义的形式化方法，然后建立公理系统，规定语言成分的有关语义。如果用一个程序P去计算自然数的阶乘，这个程序中的变量x在程序开始执行时，存放用户输入的自然数值κ；而在程序执行终止时，存放要输出的结果。用户关心的是程序P计算的结果值是否确是输入值的阶乘。在公理语义学中，使用公式｛x=κ｝P｛x=κ!｝表示程序P的这一部分含义:若P执行前x的值等于κ，则P执行完毕后 x的值等于κ!。程序P执行前的条件(x=κ)称为P的前置条件，执行后的条件(x=κ!)称为P的后置条件。这类公式称为归纳命题。一般地说，归纳命题｛R｝P｛Q｝表示：若程序P执行前，其程序变量的值满足前置条件R，则程序P执行完毕后，其程序变量的值满足后置条件Q。归纳命题用来作为描述程序有关语义的工具，公理语义学就是用归纳命题的公理系统来定义程序语言的语义。

执行赋值语句(x:=e)的结果是将程序变量x 的值变为执行该语句前表达式e的值。也就是说，执行该语句后x的值等于执行该语句前表达式e的值。因此，若表达式e在语句(x:=e)执行前满足条件R，那么程序变量x在语句(x:=e)执行完毕后亦应满足条件R。故归纳命题｛R[e/x]｝x:=e｛R｝应该永远成立。其中R[e/x]成立，表示将R中的x代为e后，R成立，即e满足R。在公理系统中，公理是一种永远成立的命题。这样采用｛R[e/x]｝ x:=e｛R｝作为公理，就表达了语句(x:=e)的语义，使用不同的R，可反映不同的用户对赋值语句语义的要求，R可以只涉及输入输出变量；也可以涉及工作单元，用来表达赋值语句的副作用。

执行顺序语句(s1;s2)，就是使用执行(s1;s2)前程序变量的值，先执行s1，然后使用执行s1后程序变量的结果值，再执行语句s2，s2执行完毕后的程序变量值，就是执行顺序语句(s1;s2)的结果值。故若执行(s1;s2)前的程序变量值满足条件R，(s1;s2)执行完毕后的值满足T，那么就可找到关于中间结果的条件Q，使得若R为s1的前置条件，则Q为s1的后置条件，而且以Q为s2的前置条件，则T就是s2的后置条件，这样就可以采用推理规则

来规定顺序语句的语义。公理系统中的推理规则表示当横线上方的命题都成立时，则横线下方的命题亦成立。人们可使用不同的R、T来表示自己所要了解的有关语义。

其他语言成分的公理语义也是用公理和推理规则类似地给出，但有的成分（如过程调用等）的语义，比起上述语句的语义要复杂得多。

论证一个程序是否具有某种含义的过程和论证一个程序是否具有某种特性的过程是完全一致的。故公理语义学是程序正确性研究的理论基础。程序验证的研究也进一步促进公理语义学的发展。

寻求适用于描述程序语义，且便于语义推导的逻辑语言是公理语义学研究的一个重要方面。70年代末出现了使用时态逻辑来定义语言的语义，称为时态语义。另外如动态逻辑、算法逻辑在语义学中的应用，也都在发展之中。