アカウント名:
パスワード:
3種類ぐらいの大分類に分かれる仕様記述言語において、Agdaは仕様の形式検証に重点が置かれているタイプ。普通なら何十パターンかのテストパターンを与えて、ブラックボックステストも十分時間をかけて行いようやく発見できるかどうかという類のバグが検証器を通せばぴたりとわかるのはすばらしい(シークエント計算なんて全くついて行けてないがチュートリアル http://unit.aist.go.jp/cvs/Agda/main.pdf [aist.go.jp]p.54とかあとagdaでググったり)
もっとも、ソフトウエアの論理の妥当性を形式検証しようという企ては歴史
至って明快な話でして。単に状態数が少ないからですよ。
惜しい、正解まで近くに居る。まさに、実用性が低い(手間が多い割りに解ける問題が少なすぎる、労力に見合わない)とみなされているから。
それはトートロジーとは違う。けど、解説するのは無駄に手間が多い割りに甲斐が少なすぎて労力に見合わないことが容易に想像できるから、これより後は自習でお願いします。
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
一つのことを行い、またそれをうまくやるプログラムを書け -- Malcolm Douglas McIlroy
もっと目をキラキラさせるべき (スコア:2, 興味深い)
3種類ぐらいの大分類に分かれる仕様記述言語において、Agdaは仕様の形式検証に重点が置かれているタイプ。
普通なら何十パターンかのテストパターンを与えて、ブラックボックステストも十分時間をかけて行いようやく発見できるかどうかという類のバグが
検証器を通せばぴたりとわかるのはすばらしい(シークエント計算なんて全くついて行けてないがチュートリアル http://unit.aist.go.jp/cvs/Agda/main.pdf [aist.go.jp]p.54とかあとagdaでググったり)
もっとも、ソフトウエアの論理の妥当性を形式検証しようという企ては歴史
Re: (スコア:0)
> 未だ現場プログラマーから冷淡な視線を浴びせられ続ける現実がこの分野の袋小路寸前の困難さを表しているのかも(汗
ハードウェアの世界では形式的検証は実用化されているのにねえ
なんでだろ
Re: (スコア:0)
至って明快な話でして。単に状態数が少ないからですよ。
Re: (スコア:0)
Re: (スコア:0)
惜しい、正解まで近くに居る。
まさに、実用性が低い(手間が多い割りに解ける問題が少なすぎる、労力に見合わない)とみなされているから。
Re: (スコア:0)
それは状態としては正しいけど、理由としては意味のないトートロジーだよ
Re: (スコア:0)
それはトートロジーとは違う。
けど、解説するのは無駄に
手間が多い割りに甲斐が少なすぎて労力に見合わない
ことが容易に想像できるから、これより後は自習でお願いします。
Re:もっと目をキラキラさせるべき (スコア:0)
学生さんは形式以外にも常識も身につけようね