関数型言語マニアのための論文紹介５：あなたのスクリプトは「常に」正しいHTMLを生成しますか？

Static Approximation of Dynamically Generated Web Pages. Yasuhiko Minamide. WWW 2005.

http://www.score.cs.tsukuba.ac.jp/~minamide/www05.pdf

実装はこちら↓（おそらく研究目的のプロトタイプですが、用途によっては実用にもなるかも？）。勝手に紹介してすみません。＞Mさん

http://www.score.is.tsukuba.ac.jp/~minamide/phpsa/

PerlなりPHPなりで、HTMLを生成するスクリプトを書いていて、「タグが閉じてないー」とか「入れ子が合わないー」とか困らないでしょうか（クロスサイトスクリプティングは言うに及ばず）。特に、そういうバグが特殊な条件でしか起こらないときは、テストで発見するのも無理だったりします。

そこで、スクリプトがどういう出力を生成するか、個々の出力ではなくプログラム自体を解析して、「このプログラムは常に正しいHTMLを生成する」といった性質を保証する、というのが上述の研究です。もちろん、チューリング完全なプログラミング言語の静的解析なので、完璧に判定できるわけはなくて（決定不能問題）、「Yesと言われたら正しい」「Noと言われたら、正しくないかもしれないし、正しいかもしれない」となります。「正しいのにNoと言われる」ケースをできるだけ減らすために、いろいろと頑張っておられます。

ちなみに、これ系の話の元を辿ると、XML処理プログラムが常にスキーマに合ったXML文書を出力するか検査する研究になります（また身内ですみません）。これも関数型言語（←これがいいたかった）。

余談：「プログラムを解析」というと「インデントが正しいことを確かめる」とか「変数の名前がわかりやすいか（人が目で）チェックする」とか思われる方々も実際にいるのですが、そういう文面上の話ではなくて、ちゃんと意味論に基づいて解析するという意味です。そもそも（PHPだろうとCだろうと）プログラミング言語に「意味」がある、という話から始めないといけませんが、それはまた今度ということでご容赦を。