アカウント名:
パスワード:
3種類ぐらいの大分類に分かれる仕様記述言語において、Agdaは仕様の形式検証に重点が置かれているタイプ。普通なら何十パターンかのテストパターンを与えて、ブラックボックステストも十分時間をかけて行いようやく発見できるかどうかという類のバグが検証器を通せばぴたりとわかるのはすばらしい(シークエント計算なんて全くついて行けてないがチュートリアルhttp://unit.aist.go.jp/cvs/Agda/main.pdf [aist.go.jp]p.54とかあとagdaでググったり)
もっとも、ソフトウエアの論理の妥当性を形式検証しようという企ては歴史がかなり古いはずなのに未だ現場プログラマーから冷淡な視線を浴びせられ続ける現実がこの分野の袋小路寸前の困難さを表しているのかも(汗
ただし、型関連の記述ミスをビルド一発で白黒つけられるという強く型付けられた言語(CやC++やC#やJava、but not JavaScript)の特質も形式検証技術の遠い親戚なはずで現場においても全く御利益を被っていないわけではない…と思う
至って明快な話でして。単に状態数が少ないからですよ。
惜しい、正解まで近くに居る。まさに、実用性が低い(手間が多い割りに解ける問題が少なすぎる、労力に見合わない)とみなされているから。
それはトートロジーとは違う。けど、解説するのは無駄に手間が多い割りに甲斐が少なすぎて労力に見合わないことが容易に想像できるから、これより後は自習でお願いします。
つまりプログラマや設計者(やその周囲のマネージャとかも含めて)の意識こそが、実用性が低いってことなんだよ!
な、なんだってーーーー!!!
ちょっと複雑(状態数が多い)な問題になるとデスマるあたりからして、冗談抜きに実用性が低いというか、自分らの実用性を高める手段を未だに見出せてないんだろうなあ。徒手空拳のまんま。プログラミング(特に言語など)の主流の発展はどちらかというと「直感的に」判り易いプログラミングのほうをまい進しているけども、ほんとにバグりにくいプログラミングのやりかたというものは、実は直感には反する方角に存在しているのかも。
すば洞
CやC++の型付けは弱いですよ。プログラマの意図の有無とは関係なしにタイプキャストしてしまうので、数値変数の型が単一でない演算のときは注意が必要(どの言語でも有効桁数の意識を持つことは必要なので、CやC++に限った話ではないですが)。注意が必要な場合があるのなら、Ocamlのように、強い型付けにより、意図的にしかタイプキ
親レスの#1643934は当エントリにおいてAgdaの方向性があまり理解されていないように見受けられたので力不足を承知で擁護に回ったものだったんですが、仕様記述言語とモデル記述言語を混同してたりいろいろしてて恥ずかしいorz
訂正のかわり→『いまさら聞けない形式手法入門』 http://monoist.atmarkit.co.jp/fembedded/special/fm/fm01.html [atmarkit.co.jp] 海外では使用記述言語の大規模な使用例もあるようで、袋小路に陥りかけという印象は間違いだったっぽいですスマンス、Agdaの言語仕様が自然言語じゃなくてAgda自身で記述されてたらマヌーな私も流石に気づいたのに惜しい!
上記引用の中にEAL7というのが出てきますが、コモンクライテリア
>インフォーマルな証明なら
逆にいえば問題はそこから先なんじゃないかな。インフォーマルな証明とフォーマルな奴とのあいだに横たわる(越えられない)壁にこそ、問題が集約してる。
変なところに嵌りこんでしまう失敗プログラム(=デスマの元)は、状態なりなんなりが「ごちゃごちゃ絡み合ってワケワカらんくなんてしまってる」ことが多いと思うけど、
たぶん、その更に元となる絡まる以前の細かい各要素じたいは、大して複雑でもなく、我々は「直感的に」こんなのフォーマルにやらなくても直感で対処できると感じ、そのとおり作業してるし、また作業できているのだろう。
ただ、(私もしょ
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
ソースを見ろ -- ある4桁UID
もっと目をキラキラさせるべき (スコア:2, 興味深い)
3種類ぐらいの大分類に分かれる仕様記述言語において、Agdaは仕様の形式検証に重点が置かれているタイプ。
普通なら何十パターンかのテストパターンを与えて、ブラックボックステストも十分時間をかけて行いようやく発見できるかどうかという類のバグが
検証器を通せばぴたりとわかるのはすばらしい(シークエント計算なんて全くついて行けてないがチュートリアルhttp://unit.aist.go.jp/cvs/Agda/main.pdf [aist.go.jp]p.54とかあとagdaでググったり)
もっとも、ソフトウエアの論理の妥当性を形式検証しようという企ては歴史がかなり古いはずなのに
未だ現場プログラマーから冷淡な視線を浴びせられ続ける現実がこの分野の袋小路寸前の困難さを表しているのかも(汗
ただし、型関連の記述ミスをビルド一発で白黒つけられるという強く型付けられた言語(CやC++やC#やJava、but not JavaScript)の特質も
形式検証技術の遠い親戚なはずで現場においても全く御利益を被っていないわけではない
…と思う
Re: (スコア:0)
> 未だ現場プログラマーから冷淡な視線を浴びせられ続ける現実がこの分野の袋小路寸前の困難さを表しているのかも(汗
ハードウェアの世界では形式的検証は実用化されているのにねえ
なんでだろ
Re: (スコア:0)
至って明快な話でして。単に状態数が少ないからですよ。
Re: (スコア:0)
Re: (スコア:0)
惜しい、正解まで近くに居る。
まさに、実用性が低い(手間が多い割りに解ける問題が少なすぎる、労力に見合わない)とみなされているから。
Re: (スコア:0)
それは状態としては正しいけど、理由としては意味のないトートロジーだよ
Re: (スコア:0)
それはトートロジーとは違う。
けど、解説するのは無駄に
手間が多い割りに甲斐が少なすぎて労力に見合わない
ことが容易に想像できるから、これより後は自習でお願いします。
Re: (スコア:0)
学生さんは形式以外にも常識も身につけようね
Re: (スコア:0)
つまりプログラマや設計者(やその周囲のマネージャとかも含めて)の意識こそが、実用性が低いってことなんだよ!
な、なんだってーーーー!!!
ちょっと複雑(状態数が多い)な問題になるとデスマるあたりからして、冗談抜きに実用性が低いというか、自分らの実用性を高める手段を未だに見出せてないんだろうなあ。徒手空拳のまんま。
プログラミング(特に言語など)の主流の発展はどちらかというと「直感的に」判り易いプログラミングのほうをまい進しているけども、ほんとにバグりにくいプログラミングのやりかたというものは、実は直感には反する方角に存在しているのかも。
Re: (スコア:0)
> 至って明快な話でして。単に状態数が少ないからですよ。
ハードウェア等の低レベルの処理は,理論的に整理された(=単純に記述できる)事を実現するために複雑な手順を行う.高級言語を使って記述されるソフトウェアの多くの部分(*1)は,現実世界の整理されていない手順を自動化するために,手順通りに記述される.
問題は,「整理されていない手順」の満たすべき制約を素朴に記述すると,往々にして手順の記述よりも長くて複雑なものになってしまうということ.これでは,検証によってプログラムが制約を満たしてい
Re: (スコア:0)
すば洞
Re: (スコア:0)
CやC++の型付けは弱いですよ。プログラマの意図の有無とは関係なしにタイプキャストしてしまうので、数値変数の型が単一でない演算のときは注意が必要(どの言語でも有効桁数の意識を持つことは必要なので、CやC++に限った話ではないですが)。注意が必要な場合があるのなら、Ocamlのように、強い型付けにより、意図的にしかタイプキ
Re:もっと目をキラキラさせるべき【訂正】 (スコア:0)
親レスの#1643934は当エントリにおいてAgdaの方向性があまり理解されていないように見受けられたので力不足を承知で擁護に回ったものだったんですが、仕様記述言語とモデル記述言語を混同してたりいろいろしてて恥ずかしいorz
訂正のかわり→『いまさら聞けない形式手法入門』 http://monoist.atmarkit.co.jp/fembedded/special/fm/fm01.html [atmarkit.co.jp]
海外では使用記述言語の大規模な使用例もあるようで、袋小路に陥りかけという印象は間違いだったっぽいですスマンス、
Agdaの言語仕様が自然言語じゃなくてAgda自身で記述されてたらマヌーな私も流石に気づいたのに惜しい!
上記引用の中にEAL7というのが出てきますが、コモンクライテリア
Re: (スコア:0)
並列や非同期プログラミングでは、デッドロックしないことやデータの一貫性の保証を、自然言語ででも証明してる人が多いのではないでしょうか。
そうでなくても、ちょっとややこしいアルゴリズムなどはコードを見て紙にメモをとりつつ正しいということを理解=証明したり、ほとんど自明に正しいコードについては、意識せずとも脳内で証明が完結したりとか。
Re: (スコア:0)
>インフォーマルな証明なら
逆にいえば問題はそこから先なんじゃないかな。
インフォーマルな証明とフォーマルな奴とのあいだに横たわる(越えられない)壁にこそ、問題が集約してる。
変なところに嵌りこんでしまう失敗プログラム(=デスマの元)は、状態なりなんなりが
「ごちゃごちゃ絡み合ってワケワカらんくなんてしまってる」
ことが多いと思うけど、
たぶん、その更に元となる絡まる以前の細かい各要素じたいは、大して複雑でもなく、
我々は「直感的に」こんなのフォーマルにやらなくても直感で対処できると感じ、
そのとおり作業してるし、また作業できているのだろう。
ただ、
(私もしょ