权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

プログラム解析のための統一型理論の構築・検証とそれに基づく解析器の自動合成

程序分析统一理论的构建与验证以及基于该理论的分析仪自动综合

基本信息

批准号：
14702063
负责人：
小林直樹
金额：
$ 9.65万
依托单位：
Tohoku University (2004)Tokyo Institute of Technology (2002-2003)
依托单位国家：
日本
项目类别：
Grant-in-Aid for Young Scientists (A)
财政年份：
2002
资助国家：
日本
起止时间：
2002 至 2004
项目状态：
已结题

项目摘要

本研究では、プログラム解析のための型理論の構築・検証(すなわち解析手法の正しさの証明)を統一的に行うための枠組みを構築し、さらにそれに基づき、構成的プログラミングの考え方を用いて解析器の自動抽出を行う手法の確立を目指している.本年度の研究成果は以下の通り.1.プログラム解析のための統一型理論の拡張・改良種々のプログラム解析を統一的に扱うための型システムとして、これまで研究してきた計算機資源使用法解析および並行プログラムの解析を拡張するとともに、並行プログラム解析器TyPiCalを実装し、そのソースプログラムをホームページ上で公開した.2.型理論に基づくプログラム解析器の抽出実験正しいプログラム解析器を自動抽出するための実験として、昨年に引き続き、一部をパラメータ化した汎用的型システムライブラリの定理証明支援器Coq上での定式化を行い、その上に単純型付きラムダ計算の定式化を行って汎用ライブラリの有効性を確かめた.昨年度に比べ、準同型写像を使ったライブラリ部分の拡充を行うなどしてライブラリの完成度を高めた.3.並行プログラムの検証のためのCoq用ライブラリの構築並行プログラムを定理証明器上で検証するためのCoq用ライブラリの作成を行った.今後は上記1番目の項目の並行プログラムの型に基づく解析の定式化を本ライブラリに組み込んでいく予定である.

This study aims to establish a unified framework for the construction, analysis, and evaluation of the model theory of the system, and to provide guidance for the establishment of an automatic extraction method for the system using the analyzer. This year's research results include the following: 1. The unified model theory for the analysis of the Internet and the improved model analysis for the analysis of the Internet and the unified model for the analysis of the use of computer resources. 2. The parallel model analysis for the analysis of the Internet and the implementation of the parallel model analyzer Typ PiCal. 2. Model theory, basic theory, extraction of the resolver, correction of the resolver, automatic extraction of the resolver, part of the model theory, general theory, theorem proving support, Coq. In addition, the calculation of the pure type of 3. The test of parallel programming is performed on the theorem prover. In the future, we will write down the parallel development of the above project.