アカウント名:
パスワード:
3種類ぐらいの大分類に分かれる仕様記述言語において、Agdaは仕様の形式検証に重点が置かれているタイプ。普通なら何十パターンかのテストパターンを与えて、ブラックボックステストも十分時間をかけて行いようやく発見できるかどうかという類のバグが検証器を通せばぴたりとわかるのはすばらしい(シークエント計算なんて全くついて行けてないがチュートリアル http://unit.aist.go.jp/cvs/Agda/main.pdf [aist.go.jp]p.54とかあとagdaでググったり)
もっとも、ソフトウエアの論理の妥当性を形式検証しようという企ては歴史
至って明快な話でして。単に状態数が少ないからですよ。
惜しい、正解まで近くに居る。まさに、実用性が低い(手間が多い割りに解ける問題が少なすぎる、労力に見合わない)とみなされているから。
それはトートロジーとは違う。けど、解説するのは無駄に手間が多い割りに甲斐が少なすぎて労力に見合わないことが容易に想像できるから、これより後は自習でお願いします。
つまりプログラマや設計者(やその周囲のマネージャとかも含めて)の意識こそが、実用性が低いってことなんだよ!
な、なんだってーーーー!!!
ちょっと複雑(状態数が多い)な問題になるとデスマるあたりからして、冗談抜きに実用性が低いというか、自分らの実用性を高める手段を未だに見出せてないんだろうなあ。徒手空拳のまんま。プログラミング(特に言語など)の主流の発展はどちらかというと「直感的に」判り易いプログラミングのほうをまい進しているけども、ほんとにバグりにくいプログラミングのやりかたというものは、実は直感には反する方角に存在しているのかも。
すば洞
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
Stableって古いって意味だっけ? -- Debian初級
もっと目をキラキラさせるべき (スコア: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)
学生さんは形式以外にも常識も身につけようね
Re: (スコア:0)
つまりプログラマや設計者(やその周囲のマネージャとかも含めて)の意識こそが、実用性が低いってことなんだよ!
な、なんだってーーーー!!!
ちょっと複雑(状態数が多い)な問題になるとデスマるあたりからして、冗談抜きに実用性が低いというか、自分らの実用性を高める手段を未だに見出せてないんだろうなあ。徒手空拳のまんま。
プログラミング(特に言語など)の主流の発展はどちらかというと「直感的に」判り易いプログラミングのほうをまい進しているけども、ほんとにバグりにくいプログラミングのやりかたというものは、実は直感には反する方角に存在しているのかも。
Re: (スコア:0)
> 至って明快な話でして。単に状態数が少ないからですよ。
ハードウェア等の低レベルの処理は,理論的に整理された(=単純に記述できる)事を実現するために複雑な手順を行う.高級言語を使って記述されるソフトウェアの多くの部分(*1)は,現実世界の整理されていない手順を自動化するために,手順通りに記述される.
問題は,「整理されていない手順」の満たすべき制約を素朴に記述すると,往々にして手順の記述よりも長くて複雑なものになってしまうということ.これでは,検証によってプログラムが制約を満たしてい
Re: (スコア:0)
すば洞