モデル生成法に基づくJavaScriptプログラム型検査の機械実行

大久保 弘崇  山本 晋一郎  坂部 俊樹  稲垣 康善  

誌名
電子情報通信学会論文誌 D   Vol.J89-D   No.4   pp.693-704
発行日: 2006/04/01
Online ISSN: 1881-0225
Print ISSN: 1880-4535
論文種別: 特集論文 (フォーマルアプローチ論文特集)
専門分野: ソフトウェア
キーワード: 
JavaScript,  型検査,  定理自動証明,  MGTP,  

本文: PDF(544.5KB)
>>論文を購入


あらまし: 
プログラムの実行の安全性を保証するために,プログラムに対する型検査がしばしば行われる.本論文では,型のないオブジェクト指向言語であるJavaScriptで書かれたプログラムの型検査について述べる.本論文の型検査は,型規則を形式的な推論規則で記述し,これを自動証明系で直接実行するアプローチを特徴とする.この方法により,型検査系の実装時の誤りがなく正確な型検査が行え,また型検査系の構築・拡張が形式的な枠組みに基づいて行える.自動証明系にはMGTPを用いた.MGTPはモデル生成法に基づく証明系で,推論規則の記述が直観的に行える.本論文では,推論規則によって定式化した型検査系をMGTPにより自動証明可能な形式で表現する方法を示す.この際,推論規則には現れない暗黙の条件である型整合性の検査規則を明示する必要があることを明らかにし,またそれをMGTP規則で表現する際の手法について述べる.