アカウント名:
パスワード:
本当に安全性を高めるなら定理証明系言語使わないとC に証明を付与する Frama-C とか ATS2 とか使って欲しい
systemdに証明の機能を取り込むべきでは?
自動定理証明 - 産業への応用 [wikipedia.org]>産業分野での応用例としては、LSIの設計とその検証が挙げられ、モデル的手法とともに使われている。Pentium FDIV バグ 以来、FPUの設計は極めて厳密に行われている。AMDやインテルはプロセッサの設計検証に自動定理証明を使っている。
ほう
よくわからないのだが、そういうのを使うと、夢物語だと言われていた「バグが無い(と証明された)プログラム」が作れるの?
動かないと証明されたプログラムは大概バグ無いよね
原理的にできない。停止性問題とか不完全性定理について調べるとよろし。「安全性を高める」のには寄与する。
だが「それを採用すれば安全性が高まる」と思考停止している馬鹿が採用した場合、不十分な学習によるミスと、過信による安全のための工程省略等が起きて安全性はむしろ下がる。
結局、安全性の高いプログラムを作れる奴でないと正しく使えないのでは、なぁ……
工業大学で、そういう系の専門を名乗るゲストの講義を聞いた事があったのだけど、定理云々以前にミス・バグまみれのコードを「正しい例」として提示していたので、そういう系は口先だけで中身はないというか結局利用者次第なんだなと実感したヨ。
証明はともかく、その上と下の両方のレイヤでミス塗れではどうにもならんわなw
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
ソースを見ろ -- ある4桁UID
安全性を高めるには (スコア:2, 興味深い)
本当に安全性を高めるなら定理証明系言語使わないと
C に証明を付与する Frama-C とか ATS2 とか使って欲しい
そこはC言語ではなく (スコア:5, おもしろおかしい)
systemdに証明の機能を取り込むべきでは?
Re:安全性を高めるには (スコア:1)
自動定理証明 - 産業への応用 [wikipedia.org]
>産業分野での応用例としては、LSIの設計とその検証が挙げられ、モデル的手法とともに使われている。Pentium FDIV バグ 以来、FPUの設計は極めて厳密に行われている。AMDやインテルはプロセッサの設計検証に自動定理証明を使っている。
ほう
Re: (スコア:0)
よくわからないのだが、そういうのを使うと、
夢物語だと言われていた「バグが無い(と証明された)プログラム」が作れるの?
Re: (スコア:0)
動かないと証明されたプログラムは大概バグ無いよね
Re: (スコア:0)
原理的にできない。停止性問題とか不完全性定理について調べるとよろし。
「安全性を高める」のには寄与する。
Re: (スコア:0)
だが「それを採用すれば安全性が高まる」と思考停止している馬鹿が採用した場合、
不十分な学習によるミスと、過信による安全のための工程省略等が起きて安全性はむしろ下がる。
結局、安全性の高いプログラムを作れる奴でないと正しく使えないのでは、なぁ……
Re: (スコア:0)
工業大学で、そういう系の専門を名乗るゲストの講義を聞いた事があったのだけど、
定理云々以前にミス・バグまみれのコードを「正しい例」として提示していたので、
そういう系は口先だけで中身はないというか結局利用者次第なんだなと実感したヨ。
証明はともかく、その上と下の両方のレイヤでミス塗れではどうにもならんわなw