JavaScript のサブセットの型システムの提案。存在しないプロパティにアクセスすると自動的に生成されたり、メソッドを更新したりできる点に対応。型なしのプログラムに型を付けるために満たすべき制約を求めて、それを解くことで型付きプログラムに変換する。「Type Inference for JavaScript」というタイトルで一人目の著者が D 論を書いてるので、そっちにも目を通すべき。

author="Christopher Anderson and Sophia Drossopoulou and Paola Giannini",
title="{Towards Type Inference for JavaScript}",
booktitle="ECOOP 2005",
publisher="Springer",
volume="3586",
series="LNCS",
pages="428--452",
year="2005"

コメント追加

投稿者 kw : 2008年4月2日 19:32:39 JST #

JavaScript の型システムの提案。クラス定義を書かない点や暗黙の型変換に対応するための工夫をしたらしい。preservation と progress が証明されている。型システムの細かいところまで読み切れていないので、また読み直したい。

author="Peter Thiemann",
title="{Towards a Type System for Analyzing JavaScript Programs}",
booktitle="ESOP 2005",
publisher="Springer",
volume="3444",
series="LNCS",
pages="408--422",
year="2005"

コメント追加

投稿者 kw : 2008年3月24日 14:44:13 JST #

Web ページに埋め込まれた JavaScript プログラムがポリシーに従っているか動的に検査する手法の提案。ポリシーはオートマトンの形で与え、検査コードを動的に埋め込む。JavaScript プログラム中で JavaScript プログラムを生成することが可能なため、動的に処理を行うことで対処する。JavaScript を簡略化した CoreScript と呼ぶモデルを構築して動作意味を定義し、検査コードの埋め込みが元にプログラムに影響しないことをフォーマルに証明。プロトタイプを実装して、簡単なポリシーに関してはうまくいくことを確かめたらしい。

author="Dachuan Yu and Ajay Chander and Nayeem Islam and Igor Serikov",
title="{JavaScript Instrumentation for Browser Security}",
booktitle="POPL 2007",
publisher="ACM Press",
pages="237--249",
year="2007"

コメント追加

投稿者 kw : 2008年3月19日 16:36:18 JST #

複数ページから構成される Web アプリケーションを Ajax 化する手法の提案。ページの抽出、スキーマに基づくページのクラスタリング、UI に着目した差分抽出などを行って最後に Ajax 化する。論文では差分のあたりの話までで、その先は今後の課題。Ajax 化することの利点が述べられていたけど、何でもかんでも Ajax 化すればいいってものでもないと思う。

author="Ali Mesbah and Arie van Deursen",
title="{Migrating Multi-page Web Applications to Single-page Ajax Interfaces}",
booktitle="Proceedings of the 11th European Conference on Software Maintenance and Reengineering",
publisher="IEEE Computer Society",
pages="181--190",
year="2007"

コメント追加

投稿者 kw : 2008年3月18日 15:38:39 JST #

Cygwin で Sapid をインストールする時に jar コマンドを使っていますが、Sun の JDK に含まれる jar にはないオプションを使っていて、gcc-java が必須でした。

コメント追加

投稿者 kw : 2008年3月5日 17:25:08 JST #

Struts アプリケーションのページ遷移を SPIN を使って検証する話。JSP と Struts 設定ファイルからページ遷移を抽出して promela 記述に落として SPIN へ。ページ遷移のノードは JSP とアクション、遷移は html:form, forward, global-forward などで、いたって普通。

author="Atsuto Kubo and Hironori Washizaki and Yoshiaki Fukazawa",
title="{Automatic Extraction and Verification of Page Transitions in a Web Application}",
booktitle="APSEC 2007",
publisher="IEEE Computer Society Press",
pages="350--357",
year="2007"

JavaCC で生成した解析器で、行にタブ文字がある時に読み取ったトークンの列番号と行頭からのバイト数が合わないと思ったら、列番号が 8 の倍数になるようにタブ文字の幅を決めるようになっていました。これで不思議だった現象は不思議ではなくなったけど、結局オフセットにはどの値を使えばいいのやら。

コメント追加

投稿者 kw : 2008年2月1日 17:58:31 JST #