04/05/04 15:15
【公理的意味論】URLﾘﾝｸ(kaiunix.cs.shinshu-u.ac.jp)
公理的意味論では意味をプログラムのセオリーとして記述する。
そしてセオリー の証明という作業を通じて、意味の正しさを確かめる。
セオリーは以下の３ つの要素から構成される
・構文規則
・公理
・推論規則
そして、プログラムαを次のような形式で表現する
{事前条件}α{事後条件}
これをpre-post式と呼ぶ。公理と推論規則はこのpre-post式を利用する。
この式は、事前条件が成り立っている(真である)という条件下でαを実行すると 事後条件が成り立つ、
と言う事を表現している。そして公理的意味論はこの 式を証明する(真偽を判定する)手段を提供している。
具体的にはαが文の列とするし、それをα1、α2、....、αnとすると、次のような式の列を順次証明する事になる
{事前条件1}α1{事後条件1}
{事前条件2}α1{事後条件2}
......
{事前条件n}αn{事後条件n}
ここで事後条件iは事前条件i+1と同じものである。
公理としては、プログラミン グ言語の各基本要素に対して、pre-post式を与える事になる。
---------------------------------------------------------------------------------------------