ポインタのあるプログラミング言語のための資源使用法解析

IPSJ Web Site

Bibliographic Information

Other Title
  • ポインタ ノ アル プログラミング ゲンゴ ノ タメ ノ シゲン シヨウホウ カイセキ
  • Resource Usage Verification for a Programming Language with Pointers

Search this article

Abstract

本論文では，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.

Journal

Related Projects

See more

Keywords

Details 詳細情報について

Report a problem

Back to top