書誌事項
- タイトル別名
-
- ポインタ ノ アル プログラミング ゲンゴ ノ タメ ノ シゲン シヨウホウ カイセキ
- Resource Usage Verification for a Programming Language with Pointers
この論文をさがす
抄録
本論文では,C言語のようなポインタのある言語に対して,計算資源の使用法を検証するための型システムを与える.この型システムに基づいて型検査を行うことにより,ファイルやメモリなどの計算資源が正しい順序でアクセスされることを自動検証することができる.我々の型システムは,小林と末永によって提案された,Cプログラムのmallocとfreeの使用法を検証するための型システムの拡張であり,その特徴は,ポインタや計算資源の型に対して所有権と呼ばれるアクセスの権限と義務を表す情報を付加したことにある.所有権を有理数で表現することにより,型検査の問題を有理数上の線形計画法に帰着し,多項式時間で解くことができる.
We propose a type system for resource usage verification of programs written in a programming language with pointers. By checking that a program is well-typed in the type system, we can verify that the program accesses resources like files and memory cells in a valid manner. Our type system is an extension of Suenaga and Kobayashi's one for checking usage of malloc/free of C programs, and the main novelty is to augment resource types with ownerships, which express both capabilities and obligations to access resources. Thanks to the use of fractions as ownerships, the type checking problem is reduced to linear programming over rational numbers, which can be solved in polynomial time.
収録刊行物
-
- 情報処理学会論文誌プログラミング(PRO)
-
情報処理学会論文誌プログラミング(PRO) 3 (4), 27-42, 2010-09-22
東京 : 情報処理学会
- Tweet
キーワード
詳細情報 詳細情報について
-
- CRID
- 1050001337899340800
-
- NII論文ID
- 110007970954
-
- NII書誌ID
- AA11464814
-
- ISSN
- 18827802
- 18827772
- 03875806
-
- NDL書誌ID
- 024298847
-
- 本文言語コード
- ja
-
- 資料種別
- article
-
- データソース種別
-
- IRDB
- NDL
- CiNii Articles
- KAKEN