アカウント名:
パスワード:
皆さんも経験ありますよね(?)
仕様通りに作るとおかしな動作になる。仕様そのものも検証対象だと学んだのが一年目
そこで形式手法ですよ数学的にプログラムのバグが無いことが証明されるその結果、仕様に多くのバグが含まれることが証明される
なんかそういう言い方をすると胡散臭く感じるけど、たいていの職業プログラマーはすでに日々形式検証のお世話になっているはず。型システムっていうんですけど。AIは実用化されるとAIと呼ばれなくなるみたいなパラドックス
型システムも、動かすまで検証されないのも普通は形式手法には含めないけど。最近のCPUは設計の一部を形式手法で検証されてるけど、ソフトではあまりないんじゃないかな。
型はコンパイルでチェックされるから「動かすまで検証されない」わけじゃないぞ確かに普通は含めないけど原理的には含まれるし、ンなことはコメ主もわかっている
静的型システム(コンパイル時に検知される)と言ったほうが良かったですかね。
残念ながらダックタイピングのため対象箇所を動かすまで検証されません。
形式手法はモデルないしアルゴリズムまでしか検証しない実装や実環境を理想化してるから実務に落とし込むならそれらとの整合性を取らないといけない聞きかじりやら理論屋(笑)はそういう面を無視するし、だから何十年たっても広まらないんだよ
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
弘法筆を選ばず、アレゲはキーボードを選ぶ -- アレゲ研究家
バグではありません!仕様です! (スコア:2, おもしろおかしい)
皆さんも経験ありますよね(?)
Re: (スコア:1)
仕様通りに作るとおかしな動作になる。仕様そのものも検証対象だと学んだのが一年目
Re:バグではありません!仕様です! (スコア:0)
そこで形式手法ですよ
数学的にプログラムのバグが無いことが証明される
その結果、仕様に多くのバグが含まれることが証明される
Re:バグではありません!仕様です! (スコア:1)
なんかそういう言い方をすると胡散臭く感じるけど、たいていの職業プログラマーはすでに日々形式検証のお世話になっているはず。型システムっていうんですけど。AIは実用化されるとAIと呼ばれなくなるみたいなパラドックス
Re:バグではありません!仕様です! (スコア:1)
型システムも、動かすまで検証されないのも普通は形式手法には含めないけど。
最近のCPUは設計の一部を形式手法で検証されてるけど、ソフトではあまりないんじゃないかな。
Re: (スコア:0)
型はコンパイルでチェックされるから「動かすまで検証されない」わけじゃないぞ
確かに普通は含めないけど原理的には含まれるし、ンなことはコメ主もわかっている
Re: (スコア:0)
静的型システム(コンパイル時に検知される)と言ったほうが良かったですかね。
Re: (スコア:0)
残念ながらダックタイピングのため対象箇所を動かすまで検証されません。
Re: (スコア:0)
形式手法はモデルないしアルゴリズムまでしか検証しない
実装や実環境を理想化してるから実務に落とし込むならそれらとの整合性を取らないといけない
聞きかじりやら理論屋(笑)はそういう面を無視するし、だから何十年たっても広まらないんだよ