アカウント名:
パスワード:
3種類ぐらいの大分類に分かれる仕様記述言語において、Agdaは仕様の形式検証に重点が置かれているタイプ。普通なら何十パターンかのテストパターンを与えて、ブラックボックステストも十分時間をかけて行いようやく発見できるかどうかという類のバグが検証器を通せばぴたりとわかるのはすばらしい(シークエント計算なんて全くついて行けてないがチュートリアル http://unit.aist.go.jp/cvs/Agda/main.pdf [aist.go.jp]p.54とかあとagdaでググったり)
もっとも、ソフトウエアの論理の妥当性を形式検証しようという企ては歴史
親レスの#1643934は当エントリにおいてAgdaの方向性があまり理解されていないように見受けられたので力不足を承知で擁護に回ったものだったんですが、仕様記述言語とモデル記述言語を混同してたりいろいろしてて恥ずかしいorz
訂正のかわり→『いまさら聞けない形式手法入門』 http://monoist.atmarkit.co.jp/fembedded/special/fm/fm01.html [atmarkit.co.jp] 海外では使用記述言語の大規模な使用例もあるようで、袋小路に陥りかけという印象は間違いだったっぽいですスマンス、Agdaの言語仕様が自然言語じゃなくてAgda自身で記述されてたらマヌーな私も流石に気づいたのに惜しい!
上記引用の中にEAL7というのが出てきますが、コモンクライテリア
>インフォーマルな証明なら
逆にいえば問題はそこから先なんじゃないかな。インフォーマルな証明とフォーマルな奴とのあいだに横たわる(越えられない)壁にこそ、問題が集約してる。
変なところに嵌りこんでしまう失敗プログラム(=デスマの元)は、状態なりなんなりが「ごちゃごちゃ絡み合ってワケワカらんくなんてしまってる」ことが多いと思うけど、
たぶん、その更に元となる絡まる以前の細かい各要素じたいは、大して複雑でもなく、我々は「直感的に」こんなのフォーマルにやらなくても直感で対処できると感じ、そのとおり作業してるし、また作業できているのだろう。
ただ、(私もしょせんは直感の世界から脱出できてない人間なので、あくまで憶測だが)その単純な各要素を組み合わせた中規模の要素が、いつ対処困難な複雑な絡み合いに化けてしまうか?については、我々の直感はあまり正確にそれを予測できていないのではないかな?
つまり「気が付けば対処困難になってやがる」という感じで。
そうなるともう、後付けではどんな手法でも(フォーマルでも)対処困難。
まともな対処方法は「もとの小ささまでバラして、再度組み立てて、そのさい非直感的な仕組みも織り込んで」なのだろうけど、直感で突っ走るのに慣れてると、なかなかそこまで戻る度胸が沸かない。
ーーーところで、あとひとつ問題があって、「非直感的な手法を正しく見つけること」に失敗してるケースも見受ける。
直感じゃなく数字なりなんなりでハッキリさせようぜ!という取り組みはしばしば見かけるんだが、不味いのはその数字の採りかたが直感(無根拠)で決められてるもんだから、結局なんの足しにもならず手間が増えてるだけ、というエセフォーマルに陥ってることが多い。
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
アレゲは一日にしてならず -- アレゲ研究家
もっと目をキラキラさせるべき (スコア:2, 興味深い)
3種類ぐらいの大分類に分かれる仕様記述言語において、Agdaは仕様の形式検証に重点が置かれているタイプ。
普通なら何十パターンかのテストパターンを与えて、ブラックボックステストも十分時間をかけて行いようやく発見できるかどうかという類のバグが
検証器を通せばぴたりとわかるのはすばらしい(シークエント計算なんて全くついて行けてないがチュートリアル http://unit.aist.go.jp/cvs/Agda/main.pdf [aist.go.jp]p.54とかあとagdaでググったり)
もっとも、ソフトウエアの論理の妥当性を形式検証しようという企ては歴史
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)
>インフォーマルな証明なら
逆にいえば問題はそこから先なんじゃないかな。
インフォーマルな証明とフォーマルな奴とのあいだに横たわる(越えられない)壁にこそ、問題が集約してる。
変なところに嵌りこんでしまう失敗プログラム(=デスマの元)は、状態なりなんなりが
「ごちゃごちゃ絡み合ってワケワカらんくなんてしまってる」
ことが多いと思うけど、
たぶん、その更に元となる絡まる以前の細かい各要素じたいは、大して複雑でもなく、
我々は「直感的に」こんなのフォーマルにやらなくても直感で対処できると感じ、
そのとおり作業してるし、また作業できているのだろう。
ただ、
(私もしょせんは直感の世界から脱出できてない人間なので、あくまで憶測だが)
その単純な各要素を組み合わせた中規模の要素が、
いつ対処困難な複雑な絡み合いに化けてしまうか?については、
我々の直感はあまり正確にそれを予測できていないのではないかな?
つまり「気が付けば対処困難になってやがる」という感じで。
そうなるともう、後付けではどんな手法でも(フォーマルでも)対処困難。
まともな対処方法は「もとの小ささまでバラして、再度組み立てて、そのさい非直感的な仕組みも織り込んで」なのだろうけど、直感で突っ走るのに慣れてると、なかなかそこまで戻る度胸が沸かない。
ーーー
ところで、あとひとつ問題があって、「非直感的な手法を正しく見つけること」に失敗してるケースも見受ける。
直感じゃなく数字なりなんなりでハッキリさせようぜ!という取り組みはしばしば見かけるんだが、
不味いのはその数字の採りかたが直感(無根拠)で決められてるもんだから、
結局なんの足しにもならず手間が増えてるだけ、というエセフォーマルに陥ってることが多い。