アカウント名:
パスワード:
正しくは、「バグが無いことを確かめる手法がない」、ということでしょうね。いわゆる悪魔の証明というやつです。
これを馬鹿正直にやろうとするのがカバレッジ率に基づく単体テストということになるのですが、これとて仕様のバグ等は取れません。また、効率が悪過ぎで、ひと目で問題の無いと分かるコードでも何通りものテストケースが必要になります。バグを効率的に取るというよりは、テストをやったというエビデンスを出すことが目的化しているように感じます。
それは「テストだから」じゃないですか?一部の形式手法ではバグがないことを保証できますよ# ただしバグの定義を書け!とか鬼畜な要求をされますけどね!
># ただしバグの定義を書け!とか鬼畜な要求をされますけどね!
それって、「プログラムを対象として見る事にして、プログラムは実行中に書き換わらないから関数型だ」とかと一緒で、実用性に欠けるとんちに見えますけど。
普通のテストなら、「うまくいく全ての」以外がバグのはずで、バグの定義を書くという事の実際の手順がさっぱり判らないです。
『「うまくいく全ての」以外がバグ』以外の定義でうまくいったからと言って、実用性が有るとは思えません。
こんなところで解説してもしょうがない気がしますが,形式手法の場合は,・「うまくいかない挙動」を定義し, 目的のシステムからそれが発生しないことを数学的に示す・うまくいくところから開始し, 起き得る動作が全て正しい動作であることを示すのどちらかが用いられます.前者の代表選手はモデル検査で, 後者の代表は証明によるソフトウェア構築(形式仕様記述も含む)でしょう.
モデル検査がそれなりに成功しているのは,マルチシステムにおいてデッドロックが発生しないことを機械的に検査できたり,例外動作の発生パスを機械的に限定できるから.
例外動作について言えば,それが本来発生してよい実行パスと, 想定していない実行パスがあったときに, 後者はバグになるでしょう.モデル検査においては「想定しているパス」を実行パスの全集合からそれを除外するだけで定義できるので, 十分に実用的です.# もちろん簡単に定義できないバグというのももちろんありますよ
自動テストとの違いは,モデル検査が異なる抽象度で検査の計算量が小さくなるように行われるのに対し,テストの場合には必ず具体的プログラムで行われるため,テストの実行時間が大きくなります.
じゃあ何も勉強してない人が形式手法が使えるか,というと, もちろんそんなことはない.なので使い分けとか役割分担が必要になる.それを考えずに, 「産業界では使えません. 実用的ではありません」と断じるのもおかしいよね# Rubyは中学生にも書けるのにJavaは書けない. Javaは実用的じゃない, と言うのと一緒
「産業界では使えません」でなく「産業界の期待はもっと大きいです」が正しいと思います。
それだけ形式化できるネタがそろっていれば、形式言語と通俗的なプログラム言語と出来ることに差が有るように見えません。RubyならRubyでJavaならJavaで、形式言語なしでも十分形式的と思います。形式言語ですごいオペレータでも発明されたら、通俗的なプログラム言語も黙ってはいないでしょうし。
訳が分からないからバグなので、それを分かる様にしてくれるのを望みます。定義されているのに実装しない抜け作は中学生だっていないと思います。
形式手法が専門だと名乗る講師の資料にコンパイルすら通らないシンタックスエラーを含むコードが正しい例として幾つも載っていたのを見て彼らは詐欺師以外の何物でもない思った。彼は単発ゲストの講師だったが、その後形式手法はしばしば話のネタになったとさ。
by 工業大学の元経営・情報系学生
かと。IC内部のマイクロプログラムとか、ライフサイクルを通してバグが顕在化しないソフトウェアは沢山在り、その内の何割かは本当にバグは無いのです。
ほんとそう思う。
バグがないソフトウェアはないって、言い訳じゃないの?
いい訳であると同時に、運用側の心構えだね。作る側は言っちゃダメ。システム運用は問題発生時の影響度が大きいからバグのないシステムは無いと想定して、運用しないといけない。それがバグのないソフトは存在しない、ということば。
開発担当が言えばただの言い訳でしょ。
開発側、運用側とか、変な壁を作らないでくださいよ。要件定義、ユーザーテストにも参画していますよね。
アプリは皆で作っているんです。こういう使い方のアプリがほしいと要望を出し、ほんとうにそう使えるかテストしているはずです。担当意識が低いと大概、こんなはずじゃなかった物ができてしまいます。
#まぁ、詭弁です。
永遠にリリースできなくなるぞ。
# もちろん既知のバグは全部とるのが前提。# バグがないことを証明する手立てがないのだから、確証を求められても困るわけで。
それだけコストと時間をかけて世に出されるソフトウェアは稀なのです。
# 簡単に差し替えできるってことは品質を落とす理由になりえるんです……
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
あと、僕は馬鹿なことをするのは嫌いですよ (わざとやるとき以外は)。-- Larry Wall
「ただし、よく知られているとおりバグのないソフトウェアは存在しない。」てのが尼杉 (スコア:2, すばらしい洞察)
Re:「ただし、よく知られているとおりバグのないソフトウェアは存在しない。」てのが尼杉 (スコア:1)
正しくは、「バグが無いことを確かめる手法がない」、ということでしょうね。いわゆる悪魔の証明というやつです。
これを馬鹿正直にやろうとするのがカバレッジ率に基づく単体テストということになるのですが、これとて仕様のバグ等は取れません。また、効率が悪過ぎで、ひと目で問題の無いと分かるコードでも何通りものテストケースが必要になります。バグを効率的に取るというよりは、テストをやったというエビデンスを出すことが目的化しているように感じます。
Re:「ただし、よく知られているとおりバグのないソフトウェアは存在しない。」てのが尼杉 (スコア:2)
それは「テストだから」じゃないですか?
一部の形式手法ではバグがないことを保証できますよ
# ただしバグの定義を書け!とか鬼畜な要求をされますけどね!
Re: (スコア:0)
># ただしバグの定義を書け!とか鬼畜な要求をされますけどね!
それって、「プログラムを対象として見る事にして、プログラムは実行中に書き換わらないから関数型だ」
とかと一緒で、実用性に欠けるとんちに見えますけど。
普通のテストなら、「うまくいく全ての」以外がバグのはずで、バグの定義を書くという事の実際の手順が
さっぱり判らないです。
『「うまくいく全ての」以外がバグ』以外の定義でうまくいったからと言って、実用性が有るとは思えません。
Re:「ただし、よく知られているとおりバグのないソフトウェアは存在しない。」てのが尼杉 (スコア:2)
こんなところで解説してもしょうがない気がしますが,
形式手法の場合は,
・「うまくいかない挙動」を定義し, 目的のシステムからそれが発生しないことを数学的に示す
・うまくいくところから開始し, 起き得る動作が全て正しい動作であることを示す
のどちらかが用いられます.
前者の代表選手はモデル検査で, 後者の代表は証明によるソフトウェア構築(形式仕様記述も含む)でしょう.
モデル検査がそれなりに成功しているのは,
マルチシステムにおいてデッドロックが発生しないことを機械的に検査できたり,
例外動作の発生パスを機械的に限定できるから.
例外動作について言えば,
それが本来発生してよい実行パスと, 想定していない実行パスがあったときに, 後者はバグになるでしょう.
モデル検査においては「想定しているパス」を実行パスの全集合からそれを除外するだけで定義できるので, 十分に実用的です.
# もちろん簡単に定義できないバグというのももちろんありますよ
自動テストとの違いは,
モデル検査が異なる抽象度で検査の計算量が小さくなるように行われるのに対し,
テストの場合には必ず具体的プログラムで行われるため,
テストの実行時間が大きくなります.
じゃあ何も勉強してない人が形式手法が使えるか,
というと, もちろんそんなことはない.
なので使い分けとか役割分担が必要になる.
それを考えずに, 「産業界では使えません. 実用的ではありません」と断じるのもおかしいよね
# Rubyは中学生にも書けるのにJavaは書けない. Javaは実用的じゃない, と言うのと一緒
Re: (スコア:0)
「産業界では使えません」でなく「産業界の期待はもっと大きいです」が正しいと思います。
それだけ形式化できるネタがそろっていれば、形式言語と通俗的なプログラム言語と出来ること
に差が有るように見えません。RubyならRubyでJavaならJavaで、形式言語なしでも十分形式的
と思います。
形式言語ですごいオペレータでも発明されたら、通俗的なプログラム言語も黙ってはいないでしょうし。
訳が分からないからバグなので、それを分かる様にしてくれるのを望みます。
定義されているのに実装しない抜け作は中学生だっていないと思います。
Re: (スコア:0)
形式手法が専門だと名乗る講師の資料にコンパイルすら通らないシンタックスエラーを含むコードが正しい例として幾つも載っていたのを見て彼らは詐欺師以外の何物でもない思った。
彼は単発ゲストの講師だったが、その後形式手法はしばしば話のネタになったとさ。
by 工業大学の元経営・情報系学生
Re: (スコア:0)
かと。IC内部のマイクロプログラムとか、ライフサイクルを通してバグが顕在化しないソフトウェアは沢山在り、その内の何割かは本当にバグは無いのです。
ほんとそう思う。
バグがないソフトウェアはないって、言い訳じゃないの?
Re:「ただし、よく知られているとおりバグのないソフトウェアは存在しない。」てのが尼杉 (スコア:1)
いい訳であると同時に、運用側の心構えだね。
作る側は言っちゃダメ。システム運用は問題発生時の影響度が大きいから
バグのないシステムは無いと想定して、運用しないといけない。それがバグのないソフトは存在しない、ということば。
開発担当が言えばただの言い訳でしょ。
Re: (スコア:0)
開発側、運用側とか、変な壁を作らないでくださいよ。
要件定義、ユーザーテストにも参画していますよね。
アプリは皆で作っているんです。
こういう使い方のアプリがほしいと要望を出し、ほんとうにそう使えるかテストしているはずです。
担当意識が低いと大概、こんなはずじゃなかった物ができてしまいます。
#まぁ、詭弁です。
Re: (スコア:0)
永遠にリリースできなくなるぞ。
# もちろん既知のバグは全部とるのが前提。
# バグがないことを証明する手立てがないのだから、確証を求められても困るわけで。
Re: (スコア:0)
それだけコストと時間をかけて世に出されるソフトウェアは稀なのです。
# 簡単に差し替えできるってことは品質を落とす理由になりえるんです……
Re: (スコア:0)
は、それこそ言い訳、口答え。リリース後に毎月「パッチ」とか聞こえは良いが実質バグ修正出し続けざるを得ない某社製品で実態は明白なのです。毎月パッチを出し続ける体力が有るなら、リリースに先立ちその体力の数割の「コストと時間をかけて世に出」せば、今日の如くの醜態には至らぬ筈です。「コストと時間をかけ」るだけでは駄目なのです。