[過去ﾛｸﾞ]
関数型プログラミング言語Haskell Part8 (994ﾚｽ)
関数型プログラミング言語Haskell Part8 http://mevius.5ch.net/test/read.cgi/tech/1193743693/
上
下
前次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
抽出解除
ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索
歴削→次ｽﾚ
栞削→次ｽﾚ
過去ﾛｸﾞﾒﾆｭｰ
895: デフォルトの名無しさん [sage] 2008/05/09(金) 20:50:23 >>891 プログラム全体の正しさを証明するのは難しすぎて(良くても面倒すぎて)実際的じゃない(少なくとも今は) だから、Haskellでもテストは手続き型言語の場合と同様に重要で、テストに代わるものは無い ただし、限定された状況では形式的な証明が有効なことはある Ordのインスタンスを書いたとき、それがちゃんと全順序になっていることを証明するとか、 自分で書いた書き換え規則(これはGHC特有の機能だけど)の正しさを証明するとか http://mevius.5ch.net/test/read.cgi/tech/1193743693/895
906: デフォルトの名無しさん [sage] 2008/05/09(金) 23:26:04 >>891 >>895 Haskellの関数と仕様を与えて、関数がその仕様をみたすことの証明をする支援ツールがある。 名前はAgda このツールによって証明された関数は、仕様を満たすことが保証されるので、テストが必要ない。 このようなツールは証明支援系(Proof Assistant)、定理証明系(Theorem Prover)などと呼ばれている。 http://mevius.5ch.net/test/read.cgi/tech/1193743693/906
907: デフォルトの名無しさん [sage] 2008/05/09(金) 23:27:45 >>891 >>895 Haskellの関数と仕様を与えて、関数がその仕様をみたすことの証明をする支援ツールがある。 名前はAgda このツールによって証明された関数は、仕様を満たすことが保証されるので、テストが必要ない。 このようなツールは証明支援系(Proof Assistant)、定理証明系(Theorem Prover)などと呼ばれている。 http://mevius.5ch.net/test/read.cgi/tech/1193743693/907
ﾒﾓ帳
(0/65535文字)
上
下
前次
1-
新
書
関
写
板
覧
索
設
栞
歴
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.030s