研究者総覧「情報知」
情報システム学専攻
- 氏 名
- 坂部 俊樹(さかべ としき)
- 講座等
- ソフトウェア論講座
- 職 名
- 教授
- 学 位
- 工学博士
- 研究分野
- プログラムの仕様記述 / 検証 / 自動生成
![](../admin/image_render_noimage.jpg)
研究内容
高品質ソフトウェアの構築技術
「高品質のソフトウェア」の条件としては、正しく動作すること、速いこと、メモリ使用量が少ないことはもちろんだが、構造が整っていていること、再利用に適していること、仕様などのドキュメントがしっかり揃っていることなど、ソフトウェア工学的な条件もあげられる。「正しく動作する」の意味はもう少し具体的に言うと、開発者の意図通りに働くこと、および、暴走やフリーズしないなどプログラムの基本的性質をもつことである。これらの高品質プログラムの条件のうち、正しく動作するという条件に注目し、プログラムが正しく動作をすることを検証する方法、正しいプログラムしかできないようなプログラム構成法などを研究課題として研究を行っている。プログラムが仕様を満たすか?という問題の研究
開発者の意図を書き表したものを仕様という。仕様は、自然言語で表現したもの、論理式として表したもの、分かり易いプログラムで表したものなど、いろいろな形式で記述される。論理式として記述される仕様の場合、それをプログラムが満たすかどうかという問題は、定理証明やモデル検査の問題として捉えられる。この研究では、仕様を等式で表し、プログラムを項書換え系という関数型プログラムのモデルとした場合の問題が帰納的定理の証明問題に帰着されることに着目し、帰納的定理自動証明法について研究を進めている。
仕様を満たすプログラムの自動生成に関する研究
プログラムの開発は段階的に行われる、つまり、既に開発済みのプログラムを拡張して新たなプログラムを開発することが多い。このような開発を自動化することがこの研究の目的である。具体的な研究課題は、既存プログラムとして項書換え系、新プログラムの仕様として限量子付き等式を採用して、それらから仕様を満たす新プログラムを自動生成する手法の開発である。現在検討している手法は、変換規則により仕様とプログラムの対を変換して、最終的に仕様を満たすプログラムを得るというものである。つまり、変換により
![](../admin/common/jyohochi/62/i0007fa(1).jpg)
を得て、最後のSnがプログラムになっていればSnがS0を満たすプログラムになるような変換規則を考案している。例えば、次のような仕様S0と既存プログラムP0を考える。
![](../admin/common/jyohochi/62/i0007fb.jpg)
![](../admin/common/jyohochi/62/i0007fc.jpg)
P0は自然数の2分の1を求める関数dのプログラム、S0は自然数の2倍を求める関数dの仕様である。このような仕様とプログラムの対(S0,P0)に変換ルールを適用するとSnとして
![](../admin/common/jyohochi/62/i0007fd.jpg)
が得られる。
プログラムが基本的性質を持つか?という問題の研究
プログラムが仕様を満たすかという問題とは別に、プログラムの基本的な性質を調べることも重要な課題である。そのような基本的な性質としては、以下のようなものがある。
1.必ず停止すること(停止性)
2.計算結果が一意になっていること(結果の一意性)
3.意図した以外には停止しないこと(デッドロックフリー性)
4.第3者にデータが洩れないこと(機密性)
5.データが改竄されないこと(保全性)
これらの性質毎に異なる検査手法が必要である。例えば、項書換え系の停止性の検査法に関する研究では、効率的にチェックできるような停止性の十分条件の研究を行っている。一方、機密性や保全性というようなプログラムの安全性のチェックには、主に、型の概念を用いる手法を研究している。
![プログラム検証、自動生成、検査システム プログラム検証、自動生成、検査システム](../admin/common/jyohochi/62/B075.jpg)
プログラム検証、自動生成、検査システム
経歴
- 1977年名大大学院工学研究科電気系専攻博士課程満了
- 1977年名大工学部助手、1985年三重大工学部助教授、
- 1987年名大工学部助教授、1993年名大工学部教授、1997年名大工学研究科教授、2003年名大情報科学研究科教授
所属学会
- 電子情報通信学会
- 日本ソフトウェア科学会
- 情報処理学会
- 人工知能学会
- EATCS
主要論文・著書
- オブジェクト指向計算モデルにおける例外処理機能の型付,コンピュータソフトウェア,20,2,2003.
- 融合変換を模倣するプログラム生成変換の戦略,電子情報通信学会技術研究報告(SS2004-33),104,466,2004.
- Partial Inversion of Constructor Term Rewriting Systems, Proc. of 16th International Symposium on Rewriting Techniques and Applications (LNCS 3467), 2005.