From: tadashi nagao <tadashi.nagao@...>
Date: 2008-02-20T19:43:49+09:00
Subject: [ruby-list:44672] Re: Ruby で形式手法

長尾です。

あいまいな議論ですみません。

ただ、
まつもとさんの書かれたように
DSLをつくるのは、意味あるような気がします。

> CafeOBJ 的というのがいまいち理解できていないのですが、「Ruby で書かれた
> プログラムを形式的に検証したい」ということだと仮定します。
>
これは、Ruby で、CafeOBJ 的なのをつくったらいいかもという意味です。

DSLの例といいたいのは、これです。ファジーでサッカーですね。
http://ozed.sourceforge.jp/about/index.html

組み込み用のDSLを形式手法を意識してRuby でつくるのは意味あるような気がします。

08/02/20 に Soutaro Matsumoto<matsumoto@soutaro.com> さんは書きました:
> 松本宗太郎といいます。
>
> > Ruby の仕様の中に、なんらかの形で、
> > 形式手法を盛り込むことは可能なのでしょうか？
>
> Ruby 言語自体の仕様、という話なら、個人的には切望しています。そのうち書
> くかも。IronRuby は、一度フォーマルな仕様を実装をモトに書き下ろし、その
> 仕様をモトに実装した、という話だそうですから、あるところにはあるのかもし
> れません。
>
> > CafeOBJ 的なことができると面白いような気がします。
>
> CafeOBJ 的というのがいまいち理解できていないのですが、「Ruby で書かれた
> プログラムを形式的に検証したい」ということだと仮定します。
>
> まず Ruby 自体の形式的な仕様が必要です。Ruby がどういう言語なのかを規定
> できないかぎり、Ruby プログラムの動作を規定することができませんから。
>
> まつもとさんが「なじまない」とフォローされてるのがどういう意味かはわかり
> ませんが、そもそも上述の理由で不可能ですし、形式的な検証にはものすごくコ
> ストが必要なので、検証を前提にするなら Ruby を採用する理由自体がなくなり
> そうな気がします。
>
> （形式的なソフトウェア検証というのは「C言語で書かれた KMP 法のプログラム
> を検証しました」といった話で、学部の卒論くらいにはなるくらいのレベルです。）
>
> （一方で、完璧な検証は不可能にしても、例えば型検査のような簡単な検査を行
> うことには、見込みはあると考えています。いずれにせよ、Ruby 自体の仕様が
> 必要ですが。）
>
> --
> Soutaro Matsumoto
>
>