- 1 名前：デフォルトの名無しさん [04/05/04 14:53]
- Lisp Scheme ML Haskell FP Mirranda など
関数型言語について話し合いましょう
関連スレ
関数型プログラミング言語ML
pc3.2ch.net/test/read.cgi/tech/1012445015/
関数型プログラミング言語Haskell
pc3.2ch.net/test/read.cgi/tech/1013846140/
LISP Scheme Part6
pc3.2ch.net/test/read.cgi/tech/1031560687/
Emacs Lisp
pc3.2ch.net/test/read.cgi/tech/1004551074/
- 10 名前：デフォルトの名無しさん [04/05/04 15:15]
- 【公理的意味論】kaiunix.cs.shinshu-u.ac.jp/Lesson/ProgLangT/2004/axiomaticsemantics.html
公理的意味論では意味をプログラムのセオリーとして記述する。
そしてセオリー の証明という作業を通じて、意味の正しさを確かめる。
セオリーは以下の３ つの要素から構成される
・構文規則
・公理
・推論規則
そして、プログラムαを次のような形式で表現する
{事前条件}α{事後条件}
これをpre-post式と呼ぶ。公理と推論規則はこのpre-post式を利用する。
この式は、事前条件が成り立っている(真である)という条件下でαを実行すると 事後条件が成り立つ、
と言う事を表現している。そして公理的意味論はこの 式を証明する(真偽を判定する)手段を提供している。
具体的にはαが文の列とするし、それをα1、α2、....、αnとすると、次のような式の列を順次証明する事になる
{事前条件1}α1{事後条件1}
{事前条件2}α1{事後条件2}
......
{事前条件n}αn{事後条件n}
ここで事後条件iは事前条件i+1と同じものである。
公理としては、プログラミン グ言語の各基本要素に対して、pre-post式を与える事になる。
---------------------------------------------------------------------------------------------
- 11 名前：デフォルトの名無しさん [04/05/04 15:17]
- では例題のプログラミング言語の定義を考える。公理的意味論の場合も個々の命 令に対してpre-post式を定義する事になる
{P(register,file)} Double_to_even {even(register) ∧ P(register/2 ,file)}
{P(register,file)} Double_to_odd {odd(register) ∧ P((register-1)/2 ,file)}
{P(register,file)} Halve {P(2*register ,file) ∨ P(2*register+1, file)}
registerは入力として与えられた変数であり、fileは実行環境における局所的な 値の集合である。またpre、postの条件におけるregisterとfileは各々 Double_to_evenの実行前と実行後の値を意味する。
--------------------------------------------------------------------------------
公理的手法はこの様に意味を定義するためのものとしてだけではなく、
プログラ ムの証明のための手段としても使われている。
すなわちプログラム全体を以下の様にpre-post式で表し、
プログラムが満たすべき条件を事後条件として、
この式を分割し、各式を証明する事により、
プログラムが正しいと言う事が 証明できた事になる、という物である
{事前条件}プログラム{事後条件}
例えばa,b,cを入力として、それを係数とする二次方程式の解をx,yに求めるプログラムをＰとすると、
その証明のための式は次の様に書ける
{a,b,cは任意の実数、但しb*b-4.0*a*c>0}P{a*x*x+b*x*c=0 AND a*y*y+b*y+c=0}
|
 |
