公理语义学

维基百科,自由的百科全书
跳到导航 跳到搜索

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

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

参见[编辑]

参考文献[编辑]