アカウント名:
パスワード:
期日に拘って納得いかない仕様を盛り込んだり、不足したりするのを潔しとしなかったことかな？
Fortran も 6x は 66 になり、7x は 77 になり、野心的な仕様の 8x は 90 になりました。その後は 95, 2000, 2003, 2008 と続いていますね。
自然言語で仕様を記述するのがそれほど難しいのなら、いっそのこと簡素なプログラミング言語（例えばLISP方言）で記述したコンパイラそのものを仕様にしてしまえばいいじゃないかこれだけ揉めた巨大仕様に基づいて現実の処理系を作ったら、混入するバグの数もハンパじゃないはずだろう？（冗談じゃなく本気でそう思うぞ）
それはLISPなどのプログラミング言語ではなくて形式手法の領域だと思います。VDM++であればコード生成までできるので考え方としてはありな気がしますが、VDM++で言語仕様を表現できるかはちょっとわかりません。
言語処理系に限らず一般的なシステムでも形式手法を使えば数桁バグの数が減るとは思うのですが、如何せん難しいのでなかなか一般的なところではお目にかかれませんね。組込方面では比較的よく利用されているらしいのですが。
モデレートされたのでついでに追記。
プログラミング言語で仕様を表現するのと形式手法で仕様を表現するのとで(仮に両方とも実現できたとして)一番の違いは、仕様の矛盾を検証できるかという点です。
通常のプログラミング言語では書かれた内容に矛盾があるかはわかりません。書かれたとおりに動くだけで、その書かれた内容がプログラム中の他の部分と矛盾があるかは判断できません。それに対して形式手法は、私の知っている限り仕様の矛盾などを検証器にかけることで自動的にあぶりだすことができます。形式手法からのコード生成は基本的にはおまけと考えていいでしょう。
また、当たり前のことですがプログラミング言語と形式手法で使われる言語では抽象度が違います。とはいっても、コード生成ができるようなVDM++などはかなりプログラム言語に近い感じを受けますが。Eiffelは言語仕様としてDbCを取り入れていますが、ほんのさわりだけですがEiffel・VDM++両方を見た感じではとても似ていました。Eiffelの作者であるBertrand Meyer氏は元々形式手法を研究していたそうなので、その点でも影響はあるのかなと思います。
自然言語で仕様を記述するのが難しい訳ではなく、仕様を練るのに掛かった時間なので関係ないと思いますよ。仕様上未定義な部分が無いかとか、矛盾しないかとか･･･リファレンス実装を基にすれば未定義はなくせますが、そうするとバグの検証が必要になり、バグの検証には仕様の検討が必要になり、結局元に戻ります。
よくある「バグではありません. 仕様です」ってのが確定的になるだけですね.
私の知り合いと同じ事を言ってますね。彼は、仕様書を書くのが面倒くさいから先にプログラムを作ってくれと仰っていました。
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
ソースを見ろ -- ある4桁UID
何が問題だったの？ (スコア:0)
ボリュームかな？ (スコア:1, 興味深い)
期日に拘って納得いかない仕様を盛り込んだり、不足したりするのを潔しとしなかったことかな？
Fortran も 6x は 66 になり、7x は 77 になり、野心的な仕様の 8x は 90 になりました。
その後は 95, 2000, 2003, 2008 と続いていますね。
Re:ボリュームかな？ (スコア:1, 興味深い)
これだけ揉めた巨大仕様に基づいて現実の処理系を作ったら、混入するバグの数もハンパじゃないはずだろう？
（冗談じゃなく本気でそう思うぞ）
Re:ボリュームかな？ (スコア:2, 興味深い)
それはLISPなどのプログラミング言語ではなくて形式手法の領域だと思います。VDM++であればコード生成までできるので考え方としてはありな気がしますが、VDM++で言語仕様を表現できるかはちょっとわかりません。
言語処理系に限らず一般的なシステムでも形式手法を使えば数桁バグの数が減るとは思うのですが、如何せん難しいのでなかなか一般的なところではお目にかかれませんね。組込方面では比較的よく利用されているらしいのですが。
Re:ボリュームかな？ (スコア:2, 興味深い)
モデレートされたのでついでに追記。
プログラミング言語で仕様を表現するのと形式手法で仕様を表現するのとで(仮に両方とも実現できたとして)一番の違いは、仕様の矛盾を検証できるかという点です。
通常のプログラミング言語では書かれた内容に矛盾があるかはわかりません。書かれたとおりに動くだけで、その書かれた内容がプログラム中の他の部分と矛盾があるかは判断できません。それに対して形式手法は、私の知っている限り仕様の矛盾などを検証器にかけることで自動的にあぶりだすことができます。形式手法からのコード生成は基本的にはおまけと考えていいでしょう。
また、当たり前のことですがプログラミング言語と形式手法で使われる言語では抽象度が違います。とはいっても、コード生成ができるようなVDM++などはかなりプログラム言語に近い感じを受けますが。
Eiffelは言語仕様としてDbCを取り入れていますが、ほんのさわりだけですがEiffel・VDM++両方を見た感じではとても似ていました。Eiffelの作者であるBertrand Meyer氏は元々形式手法を研究していたそうなので、その点でも影響はあるのかなと思います。
Re:ボリュームかな？ (スコア:1, 興味深い)
自然言語で仕様を記述するのが難しい訳ではなく、仕様を練るのに掛かった時間なので関係ないと思いますよ。
仕様上未定義な部分が無いかとか、矛盾しないかとか･･･
リファレンス実装を基にすれば未定義はなくせますが、そうするとバグの検証が必要になり、バグの検証には仕様の検討が必要になり、結局元に戻ります。
Re: (スコア:0)
＞仕様上未定義な部分が無いかとか、矛盾しないかとか･･･
ソース記述そのものを定義とすれば、少なくとも矛盾は無くなります．
＞リファレンス実装を基にすれば未定義はなくせますが、そうするとバグの検証が必要になり、バグの検証には仕様の検討が必要になり、結局元に戻ります。
ソース記述そのものを定義とすれば、バグの検証など不要です． 他の方法で記述した仕様を
Re: (スコア:0)
それだと仕様上の矛盾や予期できない挙動が定義になるだけだー
それは矛盾や予期できない挙動であってバグではないっていわれても使いにくいのには変わらない
javascriptみたいに仕様決まってるけど実装されてない（コンパイラならまだしも、エンジンがわの実装状況がまちまちで結局使えないとかより）とかよりずっとましだけどさ
Re:ボリュームかな？ (スコア:1)
よくある「バグではありません. 仕様です」ってのが確定的になるだけですね.
Re: (スコア:0)
私の知り合いと同じ事を言ってますね。
彼は、仕様書を書くのが面倒くさいから先にプログラムを作ってくれと仰っていました。