Path: sran265!katsu From: katsu@sran14.sra.co.jp (Katsuhiro Watanabe) Message-ID: Date: 24 Feb 92 13:13:57 Organization: Software Research Associates, Inc.,Japan In-reply-to: miyata@sra.co.jp's message of 4 Feb 92 03:35:41 GMT Newsgroups: sra.comp.misc Subject: Re: Formal Methods Distribution: sra References: <479@srasvf.sra.co.jp> 　sra で恐らく一番 follow が遅い渡邊＠ソフト工研です。 記事 で miyata@sra.co.jp (Shigeaki Miyata) さんいはく > ソフトウエアの設計開発に Formal-method を利用するということに > 危惧を抱いている者です。反対理由を論理的に説明するのが > 私には難しいため、現場に即した３つの事例をここにあげておきます。 　とのことで、３つの例が出ましたが、いずれも formal method の有用性を 陰に主張していると思います。 > 事例１　ユーザは大手都市銀行 > 　　　そこで相談なんだが無限ループするプログラムを発見してそのプログラムを > 　　　自動的に kill する仕掛けを作ってくれないかね？ > 形式主義者:そんなプログラムは作れないことが数学的に証明されているんだよ > 　　　　　ユーザの要求が間違っているんだ > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 　もし上の事例のプロジェクトに形式主義者がおらず、みんなで「それは 素晴らしいアイデアだ！」ということで受注して分析設計を始めてしまったら、 悲惨な結末が待っていたことでしょう。（この悲惨さに比べれば、形式主義者の 主張のせいで儲け損ねたぐらいのことは小さいことだと思います。） 私は上の例で「形式主義者がいてくれて本当によかった」と感じました。 　ただ、形式主義者が大きなお世話だったのは formal method による結果の、 T: 「そんなプログラムは作れないことが数学的に証明されているんだよ」 というところから、NON formal に C1: 「ユーザの要求が間違っているんだ」 ということを導いたところだと思います。 　プロジェクトマネージャーは、形式主義者がいう T は受け入れつつ、一方で 形式主義者が T から自分勝手に導いた C1 の方ははねつけて、 C2: 「要求定義に問題があった」 という判断（つまり、真の要求、あるいは、より適当な要求とは、無限ループを 発見することではなく、CPU 時間の無駄づかいの防止であったということ）を するべきでしょう。（後は宮田さんが現実的な解決法として示した通りです。） 　プロジェクトに、T から C1 ではなく C2 に到る能力があるかどうかは 適切なソフトウェアプロセスモデルを適用しているかどうかと関係があるかも しれません。これは formal method からはずれるし、知識がないのでやめます。 　話を宮田さんが主張したかったことに移して、 記事 で miyata@sra.co.jp (Shigeaki Miyata) さんいはく > 実は３つとも数学基礎論で不可能性が証明されている問題ですが、 > 実際の現場では簡単に解決できて、数学基礎論や形式的手法に関する事を > 何も知らない人に解かせてみると何通りもの解決方法を見つけることが > できる問題の例として出しました。 > 私が心配しているのは、形式的手法への盲信です 　例の中での形式主義者には、formal method の適用もソフトウエア開発 プロセス全体の中では道具の一つに過ぎないという視点が欠けていたと 思います。というのが、ここで盲信という言葉で表現しようとしたことの 一つの側面だと私なりに考えたのですがどうでしょう？ -- ----____----____ 渡邊克宏＠ソフトウェア工学研究所（四谷）