JavaScriptでソフトウェアの正しさを数学的厳密に証明してみた

現在、Shibuya.js が開催中です！Ustream で http://www.ustream.tv/channel/shibuyajs にて放送されています。これから、このブログの内容をしゃべります！

今回「テスト」がテーマなうえ、Shibuya.js は「役に立つ話担当」「ネタ担当」に分かれていて、僕は「ネタ担当」なんですが（笑）、いつも通りネタです。でも、遠い未来の役立つネタです！

きっかけは、id:t-wada さんに、GUIの自動テスト関係の質問をしたら、凄くいいことを教えてもらいました。

全てのテストはサンプリングテストである

（少し表現違ったらごめんなさい）話の流れで、部屋を移動しなくていけなくて、たしか、それしか話ができなかったのですが、要するに、サンプリングテストである以上、全ての入力パターンをテストすることは不可能であり、できることは、限られたコストの中で、効率よくテストする必要がある、という意味だと思います。だから、手動テスト vs 自動テスト、どっちが良いのかは、その文脈での効率性で決まるという、趣旨の発言だったと、僕は理解しました。（ちょっとしか会話できなかったので、ほとんど推測です。t-wada さんの意図は、全然違ったりして…）

この名言は、本当に凄くいい名言だと思うんですが、Shibuya.js の「ネタ担当」としては、あれ？全て？と引っかかりました (^^♪ 「例外のない規則はない」ということわざもありますしね！この、ことわざは自己矛盾しているんですが…（笑）

自動証明

というわけで、プログラムが与えられて、そのプログラムのテストプログラムが与えられて、数学的にその正しさを式変形を繰り返して、正しさを証明するプログラムを作りました！

ターゲットは、一番やりやすそうな「挿入ソート」を選びました。（申し訳ないですが、挿入ソートとは何かは、検索してください。手抜きごめんなさい）

プログラムは以下の通りです。

function sortInner(ary) {
  if (ary.length < 2) {
    return ary;
  } else {
    if (head(ary) < head(tail(ary))) {
      return ary;
    } else {
      return append(head(tail(ary)), sortInner(tail(swap(ary)));
    }
  }
}

挿入ソートは2重ループなのですが、ループの内側の部分だけです。つまり、ary[1] 以降はソート済みで、ary[0] を適切な位置まで挿入する部分をターゲットにしました。

head(ary) = ary[0]、tail(ary) = ary.slice(1)、swap(ary) は ary[0] と ary[1] を入れ替えを非破壊で（新しい配列を生成して）行います。

ソートの正しさの判定

正しくソートされていることを証明するには、以下の2つを証明する必要があります。

  1. ary[i] < ary[i + 1]
  2. 「ソート前」「ソート後」で要素が1対1対応すること

扱う問題を小さくするために、今回は、１の方だけを扱います。

というわけで、判定プログラムは以下の通りです。（isOrdered の方が正確な名前かもしれません）

function isSorted(ary) {
  if (ary.length < 2) { 
    return true; 
  } else {
    return head(ary) < head(tail(ary)) && isSorted(tail(ary));
  }
}

証明すること

証明することは、isSorted(sortInner(ARY)) = true です。前提条件として、isSorted(tail(ARY)) = true が成立します。加えて、数学的帰納法を使い証明するので（まだ、この部分は自動化できませんでした）isSorted(sortInner(tail(ARY))) = true を条件に加えます。

証明時に、変数と定数を区別しているのですが、数学的帰納法において、配列の長さは制限が加えられていて、任意の配列というわけではないので、対象の配列を定数化し、ARY で表現しました。

プログラムの表現方法

Haskell のような純粋関数型言語は難しすぎて、人間には書きづらいと思うのですが、自動証明においては、凄く扱いやすく、採用しました。関数は全て副作用がありません。つまり、配列操作は、絶対に配列を破壊しません。なので、sortInner は以下の形になります。

sortInner(ary) = 
  if(lt(len(ary), 2),
    ary,
    if (lt(head(ary), head(tail(ary)),
      ary,
      append(head(tail(ary)),
        sortInner(tail(swap(ary))))))

DOM & XPath

これをひたすら式変形します。上記の通り、関数は木構造になっているので、パターンマッチングでひたすら木構造の変形になります。

木構造をどう扱うか悩んだんですが、最初、正規表現を使おうかと思ったんですが、Perl の正規表現とは違って JavaScript の正規表現は再帰が扱えないので、木構造が扱いづらく、JavaScript (HTML) は DOM が使えて、木構造のための API があるので、関数を DOM に押し込みました！その上で、式変形のパターンマッチングを XPath を使って検索するようにしました。Firebug などを使うと、木構造の変形を追いやすく、便利でした！

定義＆公理

そのほか、使う定義や公理は以下の通り。

head(tail(swap(ary))) = head(ary)
tail(tail(swap(ary))) = tail(tail(ary))
tail(append(ary, v)) = ary
head(append(ary, v)) = v
if(true, a, b) = a
if(false, a, b) = b
if(a, b, b) = b
a && true = a
true && a = a

ちょっとズルなんですが、定義のような定理。

len(append(ary, v)) < 2 = false

連結すると、長さが2以上になるよと言う件です。len と append の関係性を手抜きしました。

上手く扱えなかった数学的帰納法

昨日・今日でこの準備をしていて、発表までに間に合わなかった、数学的帰納法の取り扱いです。以下の2つは単独で証明できると思うのですが、うまく、自動証明の流れの中で証明できなかったので、定理に加えてしまいました。ごめんなさい。次の課題として、これをちゃんと自動証明できるようにしたいです！

  1. head(tail(ARY)) < head(tail(tail(ARY)))
  2. isSorted(sortInner(head(swap(ARY)))) = true

最初の方は、tail(ARY) はソート済みだから tail(ARY)[0] < tail(ARY)[1] という事です。

次の方は、head(swap(ARY)) は長さ n – 1 だから、数学的帰納法により証明済み という事です。

if 条件の伝搬

さらに、特殊な式変形が2つ必要です。一つ目は、if (A) { B } else { C } において、B の中で A = true であることを使うことが必須です。これが、「if 条件の伝搬」。

if (A, B, C) で

  • Bの中でAを使っていたら、A = true
  • Cの中でAを使っていたら、A = false

否定形も必要でした

  • Bの中でnot Aを使っていたら、not A = false
  • Cの中でnot Aを使っていたら、not A = true

if の親関数の繰り込み

2つ目は、if の親関数の繰り込みです。 f(A ? B : C) = A ? f(B) : f(C) です。fの引数の数が任意でも扱えると言うことを上手く表現する方法が思いつかなかったので、別枠でコードを書きました。

証明戦略

式変形において、次の一手は、たくさんあり、指数関数的に増えると思ったのですが、なんと、式変形に優先順位をつけたら、一直線で証明できました。

  1. ノード数が減る変形 や if 条件の伝搬。
  2. if の親関数の繰り込み
  3. ノード数が増える変形（定義の代入）

ノード数が減る方を優先して、それをやることがなくなったら、ノードを数を増える変形をやってみて、さらに、また、ノード数を減らす変形を繰り返して、というので、できました。でも、これは、今回の特例で、おそらく、次にどういう手を繰り出すかは上手い評価関数を作って、証明が分岐していくパターンは絶対に必要だと思います。

if の親関数の繰り込み は少しだけ、木構造が複雑になる方の変形です。

デモ

というわけで、デモです。http://yukoba.jp/autotest/sort.html をごらんください。出力は、console.log() に出ます。Internet Explorer 8は未対応です（XPath の扱いが違います）。細かいアルゴリズムは http://yukoba.jp/autotest/js/sort.js をご覧ください。

というわけで、console.log() をみるとわかるのですが、なんと38回の式変形で証明できちゃうんです！

ログの出力は、「証明すべき対象の式」「使える変形式」を出力した後、そこから先は、式変形ごとに、「どの式を使って変形したか」「証明すべき対象の式の変化した結果」を繰り返し表示しています。

使用したスライド

ソフトウェアの自動証明
View more presentations from yukoba

ARM vs Intelの未来の展望

ARMはスマートフォン・携帯電話で広く使われていますが、クロック周波数の割に微妙にIntelのCPUよりも遅く、なんでなのかなーということで調べてみました。

まず、http://www.coremark.org/benchmark/index.php のベンチマークの結果から、色々数字があり、すごく悩みながら信用できそうな数字を拾ってみました。

1コア当たりの性能

名称 性能 備考
ARM Cortex-A8 600Mhz 2.035/MHz Cortex-A8は2010年のスマートフォンの主流
NVIDIA Tegra 250 1GHz 2.646/MHz Cortex-A9は2011年のスマートフォンの主流かな？
Intel Core2 Duo 1596MHz 3.205/MHz
Intel Core i5-650 3200MHz 3.244/MHz

このように、クロック当たりの性能がIntelよりも悪いです。消費電力を増やさないためだと思います。この数字が正しいとすると、今のスマートフォンの1GHzというのは、600MHzな感じです。（JavaScriptのベンチマークだと、さらに25%程度遅いイメージがあります）

今のスマートフォンの主流は Cortex-A8 ですが、これから、Cortex-A9 に移行する状態です。NVIDIA Tegra 250 は Cortex-A9 のデュアルコアで、フルハイビジョン (1080p) を再生できます。（まぁ、再生能力は、GPUの力が大きいですが…）

そして、ARMの公称値では Cortex-A8 2.0 DMIPS/MHz、Cortex-A9 2.5 DMIPS/MHz なので、CoreMark は DMIPS と数字を合わせているみたいですね。DMIPS は整数演算がどれくらい実行できるかという指標です。2.0 DMIPS/MHz というのは、1クロックあたり2回計算ができるという意味です。

2010年をにらんだARMの戦略と新CPUコア によると、Cortex-A8, Cortex-A9 は演算論理装置(ALU)が2つです。A8の 2.0 DMIPS/MHz は理屈通りですが、A9 の 25% 増しは、アウト・オブ・オーダー実行を搭載していて、命令を出てきた順番ではなく、高速に実行できるように順番を入れ替えて実行しているので、それによる効果かなと僕は思っているのですが、あんまり自信なし…。

http://journal.mycom.co.jp/articles/2010/09/10/cortex-a15/index.html によると、Cortex-A9 の次の Cortex-A15 は2013年くらいに主流になるみたいです。ALUが3つになっています。ということは、3 DMIPS/MHz 以上なるのではないかとおもいます。

ASCII.jp：詳細解説 これがSandy Bridgeのアーキテクチャーだ (3/6)｜Sandy Bridgeこと新Core iシリーズが登場 によると、Sandy Bridge は ALU が3つです。かなり昔から、IntelのCPUはALUが3つみたいです。だから、Cortex-A15 と Intel のクロック当たりの動作速度が大体同じになる気がします。

ARMのクロック当たりの動作速度は、たぶん、Cortex-A15 で Intel と同じになり一回伸び悩むようになり、クロック周波数を上げるのもチンタラになると思いますし、コア数を増やす方向に行くんでしょうねぇ。まぁ、少なくとも、Cortex-A15 が主流になる時代までは、スマートフォンはどんどん順調に速くなっていく気がします。

数年後のスマートフォンの使われ方

次期版WindowsはARMアーキテクチャをサポート - ITmedia エンタープライズ にあるように、Windows 8 や Office を ARM 対応させることを正式に発表しています。リリース時期から考えて、Cortex-A9 + メモリ1GB を最低ラインにして出荷すると思うのですが、たぶん、パフォーマンス的に問題ない気がします。2012年ならちょっと心配ですが、2013年 (Cortex-A15) なら全く問題ないと思います。

Windows の特徴として、「大きなディスプレイが必要」というアプリが中心です。大きなディスプレイというのは 1024x768 以上の事ね。純粋にスマートフォン内蔵のディスプレイで Windows や Office を使うのは非現実的ですが、スマートフォンから HDMI や無線などでディスプレイにつなぐ使い方が主流だと思います。そして、Bluetooth でキーボードやマウスとつなぎます。そういう使い方であれば、ノートパソコンがさらにダウンサイジングしただけで、一般ユーザーから見たら大差ないと思います。10インチ以上の「モバイル用ディスプレイ」というのも出回るかもしれません。

そして、スマートフォンの小さな画面用には、それ用のアプリが必要なので、今まで通り Android が使われると思います。そうすると、Android と Windows のデュアルブートになります。たぶん、端末の横にスイッチみたいのがついて、ハイバネーションして Android <-> Windows を行ったり来たりできる端末になる気がします。

数年後の話ですが、結構、この予想自信があるのですが、あたるかな〜？！

JavaScriptでVM作って「30日でできる！OS自作入門」をやってみた (2日目)

カーネル／VM Advent Calendar の40日目です。ごめんなさい1日遅れ。他の方のも面白いですよ！左のリンクからどうぞ。

私、JavaScriptでVM(仮装機械)を色々作ってきましたが、いつも、言語処理系のVMばかりで、VMwareのような、マシン自体のVMはやったことがなかったので、トライしてみました。

選んだテーマは、川合秀実さんの5年前の名著、「30日でできる! OS自作入門」。これ、凄くいい本ですね！読んでみてびっくりしました。かなりお勧めです。英訳は出ていないと思いますが、英訳を出すに値する本だと思います。でも、川合さんのOSASKは終了（中断？）しちゃっているみたいですね。

30日でできる! OS自作入門

30日でできる! OS自作入門

どうやって、VMを作るか、何時間も悩みました。OS自作入門では、NASKという川合さん自作のアセンブラとC言語で書かれています。C言語で書かれたのも一度NASKのアセンブラに変換されて、最終的にバイト列に変換されるので、NASKをターゲットにすることにしました。というわけで、やることは、CPUとBIOSの作成です。

インタープリタ方式にするか、コンパイラ方式にするかも悩んだのですが、とりあえず、コンパイラ方式にしました。NASK は LIST ファイルという、左側にバイト列があって、右側にニーモニックが出る、扱いやすい出力を作ってくれます。これを、Groovyで x86 -> JavaScript のコンパイラを作り、JavaScript に変換することにしました。本当はコンパイラを JavaScript で書きたかったのですが、ごめんなさい、手抜きです。

やってみて思ったのですが、x86 のバイト列は、命令列とデータ列が混在になっていて、コンパイルがやっかいです。NASK のアセンブラなら、データ列の部分は DB などのデータ列を表現するニーモニックを使っているので、データ列を避けてコンパイルすることができます。今回はそれに逃げています。本当にコンパイルしようと思ったら、JavaScript でJITコンパイラを作り、x86 -> JavaScript のソースコードに変換して、それを eval() で読み込むロジックが必要そうです。データとプログラムが混在するバイト列の中で、実行しようとした番地はプログラムの始まりなので、そこからJITコンパイルしていけば良さそうです。ただし、プログラムの終わりがわからないので、適当なところで中断して、そこから先も実行しようとしたら、再度コンパイルすると言う処理が必要そうです。また、プログラムの自己書き換えとかがあると、やっかいかも。

OS自作入門は、1日目はビルド方法などなので、2日目から挑戦しました。2日目は、print "\n\nhello, world\n" を実行するだけのOSです。ちなみに、3日目から32ビットモードになり、VRAMの操作が必要で、ハードルがぐんと上がります。いつか機会があったら、3日目も挑戦したいです。

あと、もう一つ愚痴。x86 って命令数がなんか多いですね！Intel® 64 and IA-32 Architectures Software Developer Manuals | Intel® Software に命令セットのマニュアルがあり、なんか、わかりにくく、x86 -> JavaScript の変換はだいぶ想像で作ってしまいました。（追記：Resource & Design Center for Development with Intel に日本語マニュアルがあるんですね）

と言うわけで、作ったファイルやデモの一覧。

  • helloos.nas - これが、元のアセンブラです。川合さんのコメントが大量に入っていてわかりやすいです。一文字ずつ読み込んで、INT 0x10 を使ってビデオBIOSを呼び出します。末尾に、RESB 1469432 という命令が入っていて、これは、サイズを1.4MBのフロッピーのサイズに揃えるために入っているのですが、これがあると次のLISTファイルの生成でエラーになるのでコメントアウトしました。
  • helloos.lst - 付属の asm.bat を書き換え、nask.exe helloos.nas helloos.img helloos.lst で生成できます。左側に番地やバイト列がつきます。
  • Compiler.groovy - これが、lst -> JavaScript のコンパイラです。前半の方で lst を読み込んで、後半の方で JavaScript を生成しています。170行程度ですし、たぶん、簡単に読めると思います。実行すると、helloos.js を生成します。
  • videoBios.js - ビデオBIOSの部分です。id が stdOut のいうDIVタグに innerHTML で追加しています。
  • helloos.js - これが、コンパイル結果です。素直にコンパイルしています。末尾に、全てのバイト列を含めていて、これを、一文字ずつ print する時に読み込んでいます。

以上により作られるデモがこれです〜！ちゃんと表示された！

helloos.html

WebSoocketではなくTCPSocketが欲しい！

JavaScript

現在、WebSocket は既存のHTTPプロキシを通した際にセキュリティ上の問題があるという理由で、Firefox 4 beta と Opera 11 で無効になっています。Chrome や Safari も悪意のある攻撃が始まったら無効にすると言っています。

そして、どのようなプロトコルにするかを IETF のメーリングリストであーだーこーだ議論されています。→ hybi Discussion Archive - Date Index

つまみ食いで読んだだけですが、話し合いは全然まとまっていないみたいです。TLSは重いからXORがいいとか、クッキーが使えるように普通のHTTPヘッダを使いたいとか、なんか色々です。（つまみ食いなので間違っていたらごめんなさい）

そもそも、既存のHTTPプロキシを通すSocketを作るというところにだいぶ無理があります。Skypeがルーター越えをするというのと同レベルの話じゃないでしょうか。バッドノウハウ過ぎて、IETFやW3Cでやるレベルのことなのだろうか？

複雑すぎる物を作ると大人数の話し合いではまとまらないというのは ECMAScript4 の反省ですが、同じ過ちを WebSocket で繰り返している気がします。

Flash には Socket クラスがあり、生の TCP が使えます。HTML5 でも TCPSocket を作って、生のTCPを使えるようにして、どうやって HTTP プロキシを通すかは、JavaScript のライブラリで解決すれば良い問題じゃないのでしょうか？

僕は、JavaScript は21世紀のC言語だと思っているのですが、仕様として用意すべき物はC言語同様、プリミティブな物にすべきだと思います。

TCPSocket と UDPSocket 作って！

（追記）ちなみに、ActionScriptでは似た話はas3corelibに入っているRFC2817Socketです。解説はここ→WordPress › Error。

中規模開発でのエクストリーム・プログラミング

アジャイル開発のエクストリーム・プログラミング(XP)は好きなんですが、開発規模が大きくなった時に、どうやるんだろう、と最近考えていて、考えをメモします。

開発規模の定義として、僕は、100行＝小規模、1万行＝中規模、100万行＝大規模と定義します。それぞれの規模でベストな手法が違います。大規模で、100人以上のメンバーがいる場合は、どうやってグループを管理するかという問題とかもあります。僕は、ほとんどが中規模開発なので、今回は、これ限定です。

エクストリーム・プログラミングを説明した最も有名な本は1999年に出た、XPエクストリーム・プログラミング入門―ソフトウェア開発の究極の手法 ですが、年々微妙に変化していて、最近の著者さんのスタンスを一番反映しているのは、http://www.extremeprogramming.org/ での説明かなと思います。

設計の終焉? でマーチン・ファウラーさんも指摘していますが、この手の手法がうまくいくかどうかは「変更コストは開発が進むにつれ増大しない」これにかかっています。古典的には、変更コストは増大する、とされているので、事前計画、つまり、設計や分析をしっかりやって、将来発生するかもしれない問題は事前にとっておこう、という発想です。それに対して、エクストリーム・プログラミングは「増大しないための工夫」を十分施こし、事前計画よりも柔軟性を重視した方が効率的である、という考えです。

問題は、「増大しないための工夫」というのが、XP本に書いてあるだけでは不完全で全てのレベルでやる必要があると思います。特に規模が、中規模以上になってくると、注意が必要です。

理論的には、規模をnとして、O(1)の変更を加えた時に、変更コストがO(1)でなければならない、というのがエクストリーム・プログラミングが成立するための前提条件です。しかし、これ、簡単に O(n) とかになりかねないです。開発にはたくさんの工程がありますが、その全ての工程でO(1)でなければいけません。一つでも、O(n) が入ると、全体が O(n) になります。ただし、nが小さい場合は、実際は O(n) であっても、それを0と見なすことで回避できちゃいます。しかし、n が大きくなるとそういう逃げは効かなくなります。

まず、わかりやすいテストから。エクストリーム・プログラミングでは自動テストを重視しています。しかも、1999年当時よりも今の方がますます自動化を重視しています。ユニットテスト（ホワイトボックステスト）と受け入れテスト（ブラックボックステスト）にわけ、どちらも、自動テストすべしとなっています。例えば、受け入れテストで、90%が自動化されていて、10%が手動の場合、この工数は、O(0.1 * n) = O(n) となり、XPの前提条件が破綻します。10%の手動テストが量が凄く少なければ0と見なせます。しかし、多いと、O(n) です。

さらに、自動テストの待ち時間も O(n) です。ここも、理論的には O(1) でなければなりません。継続的インテグレーションのためのコンピュータを用意することが推奨されていて、そちらで自動テストをやろうということになっているのですが、例えば、自動テストが複数のコンピュータで分散できるとして、待ち時間を O(1) にするには、n × 開発者数分のコンピュータが必要で、そのためのコストは、O(n * 開発者数）であり、コンピュータの代金が無視できるくらい小さいなら問題ないですが、一人あたり1万台のコンピュータとなると破綻します。（まぁ、これは考え過ぎかな）

次に、設計。今やっている作業で、どこに影響が及ぶのだろうと、コード全体を見直したら、O(n) です。XP2002カンファレンス でも間接的に触れられていますが、モジュール間がちゃんと疎結合になっていて、自分がやっているモジュールだけ考えれば良いという状態になっていないと破綻します。

実装においても、メソッド名を変更した時に、それがプログラム全域で使用されていて、それを全文置換で変換したら O(n) です。XPの前提条件を成立させるには、統合開発環境によるリファクタリングが有効である必要があります。

また、ありがちなのが、データベースのカラム名の変更。これもやっかいです。カラム名がプログラム全域に散らばっているコードは多いと思います。統合開発環境によるリファクタリングが効けばいいですが、SQLなどはできたりできなかったりします。できない場合は、DAOとして、テーブル操作を一カ所にまとめられたら、そこをいじるだけなので O(1) ですが、JOIN やサブクエリーなど複数のテーブルをまたぐ操作があると、DAO群全域に散らばってしまうので、テーブル数が O(n) とすると、変更箇所が O(n) になります。

さらに、データベースから読んだのを JSON にして、XmlHttpRequest でJavaScript に渡して、jQuery テンプレートで表示する、というフローはありがちですが、ここまで追っかけてリファクタリングしてくれる統合開発環境はないと思います。O(n) になりかねないです。

規模が大きくなるにつれ、無視できない O(n) がどんどん増えていきます。全ての工程が O(1) であることを要請するエクストリーム・プログラミングはかなり工夫と注意が必要です。

O(1) をあきらめた時にとれる方法の一つがウォーターフォールのように事前計画をしっかりやる方法ですが、計画通りに全てを遂行できるのは単純労働ですが、そういうのは過去に作ったことあるのと同じような物を作る場合なのですが、ソフトウェア業界の場合、そのようなケースでは過去のコードをいじるなり、コピー＆ペーストするなりしてしまうので、業界の仕組み的に単純労働にならないため、完璧なる事前計画をねらうのも、破綻します。

完璧なる O(1) も完璧なる事前計画も難しいです。

オールペア法で組み合わせテスト

http://orto-app.com/ のテスト＆バグ取りをずっと続けているのですが、テストする要因の組み合わせで、テスト項目数が指数関数的に爆発します。

いろいろ調べていたのですが、｢組み合わせテストをオールペア法でスピーディに！：特集｜gihyo.jp … 技術評論社」の記事がおもしろかったです。組み合わせテストといっても、第1回 組み合わせテストの技法：組み合わせテストをオールペア法でスピーディに！｜gihyo.jp … 技術評論社にあるように、3個以下の要因で発生するのが大半であり、少なくとも2個の組み合わせを全て網羅するようにして、かつ、テスト項目数を指数関数的に爆発させない方法があります。

上の記事では、PICT というソフトが紹介されていて、使ってみたら楽しかったです。

たとえば、Ortoの画面転送では、以下のような因子があるとします。

Sender: IE6, IE8, Fx3.0, Fx3.5, Fx3.6, Chrome, Safari3, Safari4, Safari5, Opera
Recver: IE6, IE8, Fx3.0, Fx3.5, Fx3.6, Chrome, Safari3, Safari4, Safari5, Opera
Net: LAN, WiMAX
App: app1, app2, app3, app4, app5, app6, app7, app8, app9, app10

これ、全部の組み合わせをテストすると、10*10*2*10 = 2000 通りありますが、pict.exe input.txt で実行すると、PICTの出力結果1 こんな感じの表が作られ、110項目になります。

110項目多いなぁ、と思い、

Sender: IE8, Fx3.6, Chrome, Safari5, Opera
Recver: IE8, Fx3.6, Chrome, Safari5, Opera
App: app1, app2, app3, app4, app5, app6, app7, app8, app9, app10

最新のブラウザ＆回線はWiMAX限定にしてみたら、PICTの出力結果2 となり、テスト数は50に減ります。

実は、思ったよりも減らなかったのですが、よく考えたら、組み合わせ爆発しないような仕組みになっているので、レガシーブラウザを切っただけでは、大きく減ることはないのですね。

おもしろかったです！

REVIVE USB - ゲームパッド自作用

小学校の親友の一人の阿部行成くんが株式会社ビット・トレード・ワンという会社をやっています。ハードウェアの会社で、電子工作の自作キットもたくさん出しています。

http://ascii.asciimw.jp/books/magazines/cover/wascii20101130.jpg

そして、彼の商品の自作用ゲームパッド「REVIVE USB」が2ページ(p.44)にわたって、週刊アスキー 2010年12月14日号に載ってます！記者さんがかぶり物のコスプレをなぜかしているので、そこも見物です（笑）。

AKIBA PC HOTLINE の記事は ゲームパッド自作用の電子工作キット登場、最大36キー、ゲーム機のコントローラもPC用に？。