リサーチユニット総覧(Research Unit Magazine)

プログラミング科学リサーチユニットScientific Study on Elegant Programming

代表者 : 亀山 幸義    中核研究者 : 前田 敦司  南出 靖彦  
他のメンバー : 海野 広志  水谷 哲也  


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







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




● TSSS (Tsukuba Software Science Seminar) 講演会シリーズの開催
● Workshop on Staged Computationの開催
● Shonan Meeting on Staged Programming Languages and HPC の開催



Scientific Study on Elegant Programming

Unit representative : Kameyama Yukiyoshi    Core researcher : Maeda Atusi  MINAMIDE Yasuhiko  
Unit members : Mizutani Tetsuya  Unno Hiroshi  
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.kameyama
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

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

Figure 2: Concepts of multi-stage programming


Social contributions and achievements

● Organization of TSSS (Tsukuba Software Science Seminar) series
● Organization of the Workshop on Staged Computation
● Organization of the Shonan Meeting on Staged Programming Languages and HPC

 (Interviewed on October 23, 2013)