From: Soutaro Matsumoto <matsumoto@...>
Date: 2008-02-20T19:07:10+09:00
Subject: [ruby-list:44671] Re: Ruby で形式手法

松本宗太郎といいます。

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

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

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

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

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

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

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

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

-- 
Soutaro Matsumoto