アカウント名:
パスワード:
正しくは、「バグが無いことを確かめる手法がない」、ということでしょうね。いわゆる悪魔の証明というやつです。
これを馬鹿正直にやろうとするのがカバレッジ率に基づく単体テストということになるのですが、これとて仕様のバグ等は取れません。また、効率が悪過ぎで、ひと目で問題の無いと分かるコードでも何通りものテストケースが必要になります。バグを効率的に取るというよりは、テストをやったというエビデンスを出すことが目的化しているように感じます。
それは「テストだから」じゃないですか?一部の形式手法ではバグがないことを保証できますよ# ただしバグの定義を書け!とか鬼畜な要求をされますけどね!
># ただしバグの定義を書け!とか鬼畜な要求をされますけどね!
それって、「プログラムを対象として見る事にして、プログラムは実行中に書き換わらないから関数型だ」とかと一緒で、実用性に欠けるとんちに見えますけど。
普通のテストなら、「うまくいく全ての」以外がバグのはずで、バグの定義を書くという事の実際の手順がさっぱり判らないです。
『「うまくいく全ての」以外がバグ』以外の定義でうまくいったからと言って、実用性が有るとは思えません。
こんなところで解説してもしょうがない気がしますが,形式手法の場合は,・「うまくいかない挙動」を定義し, 目的のシステムからそれが発生しないことを数学的に示す・うまくいくところから開始し, 起き得る動作が全て正しい動作であることを示すのどちらかが用いられます.前者の代表選手はモデル検査で, 後者の代表は証明によるソフトウェア構築(形式仕様記述も含む)でしょう.
モデル検査がそれなりに成功しているのは,マルチシステムにおいてデッドロックが発生しないことを機械的に検査できたり,例外動作の発生パスを機械的に限定できるから.
例外動作について言えば,それが本来発生してよい実行パスと, 想定していない実行パスがあったときに, 後者はバグになるでしょう.モデル検査においては「想定しているパス」を実行パスの全集合からそれを除外するだけで定義できるので, 十分に実用的です.# もちろん簡単に定義できないバグというのももちろんありますよ
自動テストとの違いは,モデル検査が異なる抽象度で検査の計算量が小さくなるように行われるのに対し,テストの場合には必ず具体的プログラムで行われるため,テストの実行時間が大きくなります.
じゃあ何も勉強してない人が形式手法が使えるか,というと, もちろんそんなことはない.なので使い分けとか役割分担が必要になる.それを考えずに, 「産業界では使えません. 実用的ではありません」と断じるのもおかしいよね# Rubyは中学生にも書けるのにJavaは書けない. Javaは実用的じゃない, と言うのと一緒
「産業界では使えません」でなく「産業界の期待はもっと大きいです」が正しいと思います。
それだけ形式化できるネタがそろっていれば、形式言語と通俗的なプログラム言語と出来ることに差が有るように見えません。RubyならRubyでJavaならJavaで、形式言語なしでも十分形式的と思います。形式言語ですごいオペレータでも発明されたら、通俗的なプログラム言語も黙ってはいないでしょうし。
訳が分からないからバグなので、それを分かる様にしてくれるのを望みます。定義されているのに実装しない抜け作は中学生だっていないと思います。
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
Stableって古いって意味だっけ？ -- Debian初級
「ただし、よく知られているとおりバグのないソフトウェアは存在しない。」てのが尼杉 (スコア:2, すばらしい洞察)
Re: (スコア:1)
正しくは、「バグが無いことを確かめる手法がない」、ということでしょうね。いわゆる悪魔の証明というやつです。
これを馬鹿正直にやろうとするのがカバレッジ率に基づく単体テストということになるのですが、これとて仕様のバグ等は取れません。また、効率が悪過ぎで、ひと目で問題の無いと分かるコードでも何通りものテストケースが必要になります。バグを効率的に取るというよりは、テストをやったというエビデンスを出すことが目的化しているように感じます。
Re: (スコア:2)
それは「テストだから」じゃないですか?
一部の形式手法ではバグがないことを保証できますよ
# ただしバグの定義を書け!とか鬼畜な要求をされますけどね!
Re:「ただし、よく知られているとおりバグのないソフトウェアは存在しない。」てのが尼杉 (スコア:0)
># ただしバグの定義を書け!とか鬼畜な要求をされますけどね!
それって、「プログラムを対象として見る事にして、プログラムは実行中に書き換わらないから関数型だ」
とかと一緒で、実用性に欠けるとんちに見えますけど。
普通のテストなら、「うまくいく全ての」以外がバグのはずで、バグの定義を書くという事の実際の手順が
さっぱり判らないです。
『「うまくいく全ての」以外がバグ』以外の定義でうまくいったからと言って、実用性が有るとは思えません。
Re:「ただし、よく知られているとおりバグのないソフトウェアは存在しない。」てのが尼杉 (スコア:2)
こんなところで解説してもしょうがない気がしますが,
形式手法の場合は,
・「うまくいかない挙動」を定義し, 目的のシステムからそれが発生しないことを数学的に示す
・うまくいくところから開始し, 起き得る動作が全て正しい動作であることを示す
のどちらかが用いられます.
前者の代表選手はモデル検査で, 後者の代表は証明によるソフトウェア構築(形式仕様記述も含む)でしょう.
モデル検査がそれなりに成功しているのは,
マルチシステムにおいてデッドロックが発生しないことを機械的に検査できたり,
例外動作の発生パスを機械的に限定できるから.
例外動作について言えば,
それが本来発生してよい実行パスと, 想定していない実行パスがあったときに, 後者はバグになるでしょう.
モデル検査においては「想定しているパス」を実行パスの全集合からそれを除外するだけで定義できるので, 十分に実用的です.
# もちろん簡単に定義できないバグというのももちろんありますよ
自動テストとの違いは,
モデル検査が異なる抽象度で検査の計算量が小さくなるように行われるのに対し,
テストの場合には必ず具体的プログラムで行われるため,
テストの実行時間が大きくなります.
じゃあ何も勉強してない人が形式手法が使えるか,
というと, もちろんそんなことはない.
なので使い分けとか役割分担が必要になる.
それを考えずに, 「産業界では使えません. 実用的ではありません」と断じるのもおかしいよね
# Rubyは中学生にも書けるのにJavaは書けない. Javaは実用的じゃない, と言うのと一緒
Re: (スコア:0)
「産業界では使えません」でなく「産業界の期待はもっと大きいです」が正しいと思います。
それだけ形式化できるネタがそろっていれば、形式言語と通俗的なプログラム言語と出来ること
に差が有るように見えません。RubyならRubyでJavaならJavaで、形式言語なしでも十分形式的
と思います。
形式言語ですごいオペレータでも発明されたら、通俗的なプログラム言語も黙ってはいないでしょうし。
訳が分からないからバグなので、それを分かる様にしてくれるのを望みます。
定義されているのに実装しない抜け作は中学生だっていないと思います。