アカウント名:
パスワード:
皆さんも経験ありますよね(?)
仕様通りに作るとおかしな動作になる。仕様そのものも検証対象だと学んだのが一年目
そこで形式手法ですよ数学的にプログラムのバグが無いことが証明されるその結果、仕様に多くのバグが含まれることが証明される
なんかそういう言い方をすると胡散臭く感じるけど、たいていの職業プログラマーはすでに日々形式検証のお世話になっているはず。型システムっていうんですけど。AIは実用化されるとAIと呼ばれなくなるみたいなパラドックス
型システムも、動かすまで検証されないのも普通は形式手法には含めないけど。最近のCPUは設計の一部を形式手法で検証されてるけど、ソフトではあまりないんじゃないかな。
型はコンパイルでチェックされるから「動かすまで検証されない」わけじゃないぞ確かに普通は含めないけど原理的には含まれるし、ンなことはコメ主もわかっている
静的型システム(コンパイル時に検知される)と言ったほうが良かったですかね。
残念ながらダックタイピングのため対象箇所を動かすまで検証されません。
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
未知のハックに一心不乱に取り組んだ結果、私は自然の法則を変えてしまった -- あるハッカー
バグではありません!仕様です! (スコア:2, おもしろおかしい)
皆さんも経験ありますよね(?)
Re: (スコア:1)
仕様通りに作るとおかしな動作になる。仕様そのものも検証対象だと学んだのが一年目
Re: (スコア:0)
そこで形式手法ですよ
数学的にプログラムのバグが無いことが証明される
その結果、仕様に多くのバグが含まれることが証明される
Re:バグではありません!仕様です! (スコア:1)
なんかそういう言い方をすると胡散臭く感じるけど、たいていの職業プログラマーはすでに日々形式検証のお世話になっているはず。型システムっていうんですけど。AIは実用化されるとAIと呼ばれなくなるみたいなパラドックス
Re:バグではありません!仕様です! (スコア:1)
型システムも、動かすまで検証されないのも普通は形式手法には含めないけど。
最近のCPUは設計の一部を形式手法で検証されてるけど、ソフトではあまりないんじゃないかな。
Re: (スコア:0)
型はコンパイルでチェックされるから「動かすまで検証されない」わけじゃないぞ
確かに普通は含めないけど原理的には含まれるし、ンなことはコメ主もわかっている
Re: (スコア:0)
静的型システム(コンパイル時に検知される)と言ったほうが良かったですかね。
Re: (スコア:0)
残念ながらダックタイピングのため対象箇所を動かすまで検証されません。