| 講演名 | 2004/5/7 形式的手法に基づくJavaScriptプログラムの型検査系の実現 大久保 弘崇, 山本 晋一郎, 坂部 俊樹, 稲垣 康善, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 我々は,形式的手法の実際的応用を目指し,次の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. |
| キーワード(和) | JavaScript / 型検査 / 推論系 |
| キーワード(英) | JavaScript / type inference / theorem prover |
| 資料番号 | SS2004-3 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2004/5/7(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 形式的手法に基づくJavaScriptプログラムの型検査系の実現 |
| サブタイトル（和） | |
| タイトル（英） | A Formal Approach to Type Inference System for JavaScript Programs |
| サブタイトル（和） | |
| キーワード(1)（和/英） | JavaScript / JavaScript |
| キーワード(2)（和/英） | 型検査 / type inference |
| キーワード(3)（和/英） | 推論系 / theorem prover |
| 第 1 著者 氏名（和/英） | 大久保 弘崇 / Hirotaka OHKUBO |
| 第 1 著者 所属（和/英） | 愛知県立大学情報科学部 Aichi Prefectural University, Faculty of Information Science and Technology |
| 第 2 著者 氏名（和/英） | 山本 晋一郎 / Shinichiro YAMAMOTO |
| 第 2 著者 所属（和/英） | 愛知県立大学情報科学部 Aichi Prefectural University, Faculty of Information Science and Technology |
| 第 3 著者 氏名（和/英） | 坂部 俊樹 / Toshiki SAKABE |
| 第 3 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Nagoya University, Graduate School of Information Science |
| 第 4 著者 氏名（和/英） | 稲垣 康善 / Yasuyoshi INAGAKI |
| 第 4 著者 所属（和/英） | 愛知県立大学情報科学部 Aichi Prefectural University, Faculty of Information Science and Technology |
| 発表年月日 | 2004/5/7 |
| 資料番号 | SS2004-3 |
| 巻番号（vol） | vol.104 |
| 号番号（no） | 47 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |