2008年2月20日

[ruby-list:44671] Re: Ruby で形式手法

松本宗太郎といいます。

> Ruby の仕様の中に、なんらかの形で、
> 形式手法を盛り込むことは可能なのでしょうか?

Ruby 言語自体の仕様、という話なら、個人的には切望しています。そのうち書
くかも。IronRuby は、一度フォーマルな仕様を実装をモトに書き下ろし、その
仕様をモトに実装した、という話だそうですから、あるところにはあるのかもし

れません。

> CafeOBJ 的なことができると面白いような気がします。

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

まず Ruby 自体の形式的な仕様が必要です。Ruby がどういう言語なのかを規定
できないかぎり、Ruby プログラムの動作を規定することができませんから。

まつもとさんが「なじまない」とフォローされてるのがどういう意味かはわかり
ませんが、そもそも上述の理由で不可能ですし、形式的な検証にはものすごくコ
ストが必要なので、検証を前提にするなら Ruby を採用する理由自体がなくなり
そうな気がします。

(形式的なソフトウェア検証というのは「C言語で書かれた KMP 法のプログラム
を検証しました」といった話で、学部の卒論くらいにはなるくらいのレベルです。)

(一方で、完璧な検証は不可能にしても、例えば型検査のような簡単な検査を行
うことには、見込みはあると考えています。いずれにせよ、Ruby 自体の仕様が
必要ですが。)

--
Soutaro Matsumoto

投稿者 xml-rpc : 2008年2月20日 19:07
役に立ちました?:
過去のフィードバック 平均:(0) 総合:(0) 投票回数:(0)
本記事へのTrackback: http://hoop.euqset.org/blog/mt-tb2006.cgi/70020
トラックバック
コメント
コメントする




画像の中に見える文字を入力してください。