研究室公開
OPEN LABORATORY
コミュニケーションの未来
電気通信研究所
07
ヒトとコンピュータのギャップを埋める
プログラミングに対する形式的アプローチ
|
中野研究室 |
EXHIBIT
オープンキャンパスでの展示
コンピュータの無限の動作を有限の時間で保証する
ヒトはコンピュータに実行してほしいことを伝えるためには「プログラム」を記述しますが，そのプログラムが意図通りに動作することを確認するのは簡単ではありません． 多くのプログラマはいくつかの入力について試験的に実行することで確認するだけです． しかし，それで本当に正しいと言えるでしょうか？ 実際の入力には無限の可能性があり，いくら実行してもこの方法では確実に正しいとは言い切れません． この展示では入力に無限の可能性がある場合でも，有限時間でプログラムの正しさを確認する方法を紹介します．
私たちの研究
LABORATORY
プログラミングにおけるヒトの思考とコンピュータによる計算の枠組みのギャップを埋める研究
ヒトの思考に合わせて記述したプログラムは，必ずしもコンピュータにとって実行しやすいものとは限りません．プログラムを効率よく実行するには，コンピュータの枠組みに合わせて複雑なプログラムを記述する必要があります．本研究室では，このような「複雑であるが効率のよいプログラム」を「ヒトの思考に沿ったプログラム」から自動的に導出するプログラム変換や，「効率のために複雑に記述されたプログラム」がヒトの意図通りに動作することを保証するプログラム検証の研究に取り組んでいます．
形式木言語理論を利用したプログラム変換とプログラム検証
コンピュータの扱う多くのデータは木構造として捉えることができ，それらを扱うプログラムは木構造変換と考えることができます． 形式木言語理論は木構造データを形式的に扱うためのもので，この理論の結果を利用して木構造を対象とするプログラムの効率化 (変換) や静的型検査 (検証) を実現することができます． また，ある特定の形をした木構造変換であれば等価性判定が可能であることが知られていて，これを応用すると2つのプログラムが同じ入力に対して必ず同じ出力を返すことを自動的に確認することができます．また，定理証明支援系を用いてこれらの理論の形式化を進めています．
