公理語義學(Axiomatic semantics)是使用數理邏輯來證明程序正確性。程序中的命令的意義描述是通過對程序狀態(state)的斷言(assertion)效果。斷言是邏輯語句——帶變量的謂詞,而這些變量定義了程序的狀態。

公理語義學的一個實例是霍爾邏輯

參見

編輯

參考文獻

編輯