公理語義學（Axiomatic semantics）是使用數理邏輯來證明程序正確性。程序中的命令的意義描述是通過對程序狀態的斷言（assertion）效果。斷言是邏輯語句——帶變量的謂詞，而這些變量定義了程序的狀態。
公理語義學的一個實例是霍爾邏輯。
