公理的意味論

axiomatic semantics

語句の並びに論理学的公理を適用することで意味を明らかにする

語句の意味とそれを表す論理式を区別しない

プログラムに関する何らかの言明を道ビック溜めの論理体系を構築することで、プログラムの意味を与える

言語の定義として法則自身を取る

項の意味は、その項について証明できる事実である

プログラムに関する推論のプロセスに専心している

Hoareの体系の推論規則を通してプログラムの意味を与える物

例

不変条件とか

参考