キーワード：プログラム言語、ソフトウェア検証、言語処理系、メタプログラミング、高信頼ソフトウェア

　家電、PC、携帯 電話、ゲームなど、私たちの身の回りにはプログラムで動いている機械がたくさん存在しています。ロケットや車といったモノの設計をする際、部品数を10倍にする人はいませんが、コンピュータプログラムの場合は、実態が見えにくいため、開発者が意識して減らさない限りどんどん長大かつ複雑になってしまいます。100万行以上のコードからなるプログラムも少なくなく、整合性を欠いたプログラムが、性能・機能・信頼性低下を引き起こすこともあります。「プログラミング科学」リサーチユニットは、正しいプログラムはコンパクトで美しい、をモットーに、メンバー一丸となって信頼性の高いプログラム作りに取り組んで います。

プログラミングを科学する

プログラムというと複雑なものをイメージされるかもしれませんが、数学を用いることで非常にスマートになり、また、応用範囲も広がります。ソフトウェアでもっとも大切なことは、正しく動く、つまり、信頼性を保証することです。信号で例えると、最も安全な信号は赤です。赤信号は完璧な信頼性を持つ、といえますがこのままでは意味がありません。私たちは信頼性を保ったうえで、車のトラフィックを最大限にするソフトウエアを開発したい。そのために、科学的・系統的な方法を用いてプログラミングを科学しています。そのほかに、私たちは正しいが非常に効率の悪いプログラムを、効率の良いプログラムへと変換したり、また、ゼロから正しいプログラムを自動的に作るマルチステージプログラミングにも挑戦しています。

プログラムの信頼性を検証するシステムを構築する

現在のコンピュータプログラムが巨大かつ複雑に進化している理由の一つは、プログラムを使う側の要望に沿った専門的な開発が随時進んでいるせいです。ハードウェアごとに異なるソフトウェアが開発されたりもしています。これはメンテナンス面からみると非常に具合いが悪く、またプログラムの信頼性低下にもつな がります。そこで、私たちはプログラム生成器を使って多段階でプログラムをつくるマルチステージプログラミング（MSP）に注目しています。従来の研究では、効率良いプログラム生成に不可欠な「エフェクト」*1を持つ場合、MSPで生成されたプログラムの信頼性の保証が全くできませんでした。私たちは、エフェクトを持つプログラムの場合でも、MSPにおける信頼性を保証する方法を発見しました。プログラムの信頼性には、整数と文字列の足し算をしない、といった簡単なものから、どんな入力に対してもプログラムが停止して想定通りの答えを返すという正当性まで、たくさんのレベルがあります。今後も科学的なアプローチでプログラムの信頼性を提供する、という形で、使う側にいるプログラマと協力していきたいと思っています。

 (取材：平成25年10月23日)

Key words: programming language, software verification, language processing system, metaprogramming, highly reliable software

    Computer programs abound in our lives, embedded in a variety of equipment and devices such as electric appliances, PCs, mobile phones, and gaming devices.
To make our lives more convenient, computer programs tend to become large and complex unless the developers are careful enough to structure the code in a principled way. It is not uncommon for computer programs to be more than one million lines of code, and the inconsistency of a program may compromise the performance, functionality, and reliability of the whole information system. Research Unit on Theory and Practice of Programming aims at developing the highly reliable computer programs. Our slogan is “Correct programs are simple and beautiful”.

Programming as a scientific discipline

Computer programs are considered large and complex. However, simpler and more applicable programs can be developed by incorporating mathematics into them. The most important issue for software is its correctness, or assured reliability. However, reliability alone does not make sense. For example, a traffic signal is guaranteed to be safe, if it is always red (“don’t go”), but this safety is meaningless, and we want to have a traffic signal which allows maximal traffic while ensuring its safety. Similarly, our goal is to develop highly reliable, highly functioning, and high performant programs, and the research unit conducts scientific research on programming, using scientific and systematic approaches. Our research activities also include program transformation, program synthesis, and program verification.

Figure 1: Requirements to software

Building systems that verify programs

Current computer programs are becoming increasingly larger and more complex, partly because specialized development has been done to address their users’ divergent requests. Often many different versions of a single software are developed for different types of hardware. This is not only inconvenient from the perspective of maintenance, but it may also reduce the reliability of programs. To solve these problems, the research unit focuses on multi-stage programing (MSP), in which we write a code-generator, which, when executed, generates code specialized in specific domain or hardware, and then the generated code is executed to produce the final results. Previous studies could not establish the reliability of MSP-based programs with computational effects,*1 which are essential for the efficiency of the generated code The problem remained open for more than ten years, and for the first time in the world, we have developed a method for establishing the reliability of multi-stage programs with computational effects. The research unit continues the efforts to enhance the reliability of programs based on scientific approaches.

Figure 2: Concepts of multi-stage programming