公理语义学

公理语义学（Axiomatic semantics）是使用数理逻辑来证明程序正确性。程序中的命令的意义描述是通过对程序状态(state)的断言（assertion）效果。断言是逻辑语句——带变量的谓词，而这些变量定义了程序的状态。

公理语义学的一个实例是霍尔逻辑。

参见

• 代数语义学（英语：Algebraic semantics (computer science)）
• 指称语义学
• 操作语义学
• 形式语义学
• 谓词变换语义学（英语：Predicate transformer semantics）
• 断言 (程式)

参考文献