アカウント名:
パスワード:
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のように、強い型付けにより、意図的にしかタイプキャストできない方が安全。
また、基底クラスで宣言しておいて、派生クラスのインスタンスを代入できてしまうので、プログラマがタイプキャストの前に意図的に型のチェックをするか、仮想関数を使用して、タイプキャストそのものの使用を避けないと、挙動の予測できないコードができてしまいます。でも、そうやって誤ったタイプキャストを避けることはできても、コード上でそのオブジェクトが基底クラスのインスタンスか、派生クラスのインスタンスか、ということは分からないことがあります。そういった場合には、CやC++の型宣言はほとんど無意味。
CやC++で型宣言があるのは、それがないとコンパイルできないからであって、プログラマのミスを防ごうという高尚な目的のためではないと思います。動的型付けであっても、実行できてしまうからと言って、機械的なチェックが全くできないわけではないですし。それに、型以上の引数のチェックを行うとすると、静的型付けの言語でも実行時のチェックしかできません。その型以上のチェックというのは、通常の言語であれば任意ですが、Agdaの場合は、その型以上のチェックも型宣言に含まれてしまっているのかな。
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
ソースを見ろ -- ある4桁UID
もっと目をキラキラさせるべき (スコア:2, 興味深い)
3種類ぐらいの大分類に分かれる仕様記述言語において、Agdaは仕様の形式検証に重点が置かれているタイプ。
普通なら何十パターンかのテストパターンを与えて、ブラックボックステストも十分時間をかけて行いようやく発見できるかどうかという類のバグが
検証器を通せばぴたりとわかるのはすばらしい(シークエント計算なんて全くついて行けてないがチュートリアル http://unit.aist.go.jp/cvs/Agda/main.pdf [aist.go.jp]p.54とかあとagdaでググったり)
もっとも、ソフトウエアの論理の妥当性を形式検証しようという企ては歴史
Re:もっと目をキラキラさせるべき (スコア:0)
CやC++の型付けは弱いですよ。プログラマの意図の有無とは関係なしにタイプキャストしてしまうので、数値変数の型が単一でない演算のときは注意が必要(どの言語でも有効桁数の意識を持つことは必要なので、CやC++に限った話ではないですが)。注意が必要な場合があるのなら、Ocamlのように、強い型付けにより、意図的にしかタイプキャストできない方が安全。
また、基底クラスで宣言しておいて、派生クラスのインスタンスを代入できてしまうので、プログラマがタイプキャストの前に意図的に型のチェックをするか、仮想関数を使用して、タイプキャストそのものの使用を避けないと、挙動の予測できないコードができてしまいます。でも、そうやって誤ったタイプキャストを避けることはできても、コード上でそのオブジェクトが基底クラスのインスタンスか、派生クラスのインスタンスか、ということは分からないことがあります。そういった場合には、CやC++の型宣言はほとんど無意味。
CやC++で型宣言があるのは、それがないとコンパイルできないからであって、プログラマのミスを防ごうという高尚な目的のためではないと思います。動的型付けであっても、実行できてしまうからと言って、機械的なチェックが全くできないわけではないですし。それに、型以上の引数のチェックを行うとすると、静的型付けの言語でも実行時のチェックしかできません。その型以上のチェックというのは、通常の言語であれば任意ですが、Agdaの場合は、その型以上のチェックも型宣言に含まれてしまっているのかな。