形式的手法に基づくJavaScriptプログラムの型検査系の実現
スポンサーリンク
概要
- 論文の詳細を見る
我々は,形式的手法の実際的応用を目指し,次の3つの視点から研究を進めている.第1は,型のないオブジェクト指向言語であるJavaScriptに対する型検査手法を提案すること.この型検査により,JavaScriptプログラムの安全性を高めることができる.第2は,ソフトウェア工学の問題に汎用の定理証明系を適用することにより,形式的手法を現実的な問題に直接適用する可能性を探ること.このため,型検査系を推論規則により形式的に定義し,これを極力そのままの形で実際のプログラムに適用する.第3は,上の目的に適合する定理証明系のための言語を提案すること.ソフトウェア工学の現実的な問題に定理証明系を適用する際に必要となるシンタックスシュガーや演算定義能力についての知見を得る.本稿では,JavaScriptのサブセット言語に対する単純な型推論系に基づいて,モデル生成型の定理証明系による自動証明による型検査を試みる.
- 2004-05-07
著者
-
大久保 弘崇
愛知県立大学情報科学部
-
山本 晋一郎
愛知県立大学情報科学部
-
坂部 俊樹
名古屋大学大学院情報科学研究科
-
稲垣 康善
豊橋技術科学大学
-
稲垣 康善
愛知県立大学情報科学部
-
大久保弘崇
愛知県立大学
-
山本 晋一郎
愛知県立大学
-
大久保 弘崇
名古屋大学情報工学科
-
大久保 弘崇
愛知県立大学
-
坂部 俊樹
名古屋大学大学院 情報科学研究科
-
大久保 弘崇
愛知県立大学大学院情報科学研究科
関連論文
- 基本対称関数に基づく節をもつCNF論理式の充足可能性判定(計算論,計算モデル)
- 拡張可能ソフトウェアの動作情報を用いたプラグイン開発支援(開発支援(学生セッション))
- ウインターワークショップ2008・イン・道後開催報告
- ビットエラー通信路におけるスケーラブルCANの動作解析
- 右線形右シャローな項書換え系における文脈依存停止性の決定可能性について (ソフトウェアサイエンス)
- シャローな依存対から構成される項書換え系の停止性の決定可能性
- 基本対称関数を付加したCNF論理式の充足可能性判定
- 制約付き項書換え系の定理自動証明における等式の方向付けのための簡約化順序
- プレスブルガー文付き項書換え系における書換え帰納法について
- 例外処理付きオブジェクト指向プログラムにおける情報流の安全性解析のための型システム(ディペンダブルコンピューティング)