形式的手法に基づく JavaScript プログラムの型検査系の実現 A Formal Approach to Type Inference System for JavaScript Programs

この論文をさがす

著者

抄録

我々は,形式的手法の実際的応用を目指し,次の3つの視点から研究を進めている.第1は,型のないオブジェクト指向言語であるJavaScriptに対する型検査手法を提案すること.この型検査により,JavaScriptプログラムの安全性を高めることができる.第2は,ソフトウェア工学の問題に汎用の定理証明系を適用することにより,形式的手法を現実的な問題に直接適用する可能性を探ること.このため,型検査系を推論規則により形式的に定義し,これを極力そのままの形で実際のプログラムに適用する.第3は,上の目的に適合する定理証明系のための言語を提案すること.ソフトウェア工学の現実的な問題に定理証明系を適用する際に必要となるシンタックスシュガーや演算定義能力についての知見を得る.本稿では,JavaScriptのサブセット言語に対する単純な型推論系に基づいて,モデル生成型の定理証明系による自動証明による型検査を試みる.

We investigate application of formal methods to practical type inference problems from the following three view points: The first point is to propose a type checking method for programs in JavaScript, which is an untyped object-oriented language. Type checking improves the safety of JavaScript programs. The second is to explore the possibility of applying formal methods to practical problems through applying general purpose theorem prover to a problem of software engineering. The third is to propose a language for theorem provers suitable for our purpose. This paper reports our investigation of constructing a simple type inference system for a subset of JavaScript by using a theorem prover based on model generation.

収録刊行物

  • 電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス

    電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 104(47), 13-18, 2004-05-07

    一般社団法人電子情報通信学会

参考文献:  8件中 1-8件 を表示

被引用文献:  1件中 1-1件 を表示

キーワード

各種コード

  • NII論文ID(NAID)
    110003276734
  • NII書誌ID(NCID)
    AN10013287
  • 本文言語コード
    JPN
  • 資料種別
    ART
  • ISSN
    09135685
  • NDL 記事登録ID
    6995573
  • NDL 雑誌分類
    ZN33(科学技術--電気工学・電気機械工業--電子工学・電気通信)
  • NDL 請求記号
    Z16-940
  • データ提供元
    CJP書誌  CJP引用  NDL  NII-ELS 
ページトップへ