公理語義學

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

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

參見

• 代數語義學（英語：Algebraic semantics (computer science)）
• 指稱語義學
• 操作語義學
• 形式語義學
• 謂詞變換語義學（英語：Predicate transformer semantics）
• 斷言 (程式)

參考文獻