PR
三日目の基調講演を担当したSenior Vice President, Microsoft ResearchのRick Rashid氏
三日目の基調講演を担当したSenior Vice President, Microsoft ResearchのRick Rashid氏
[画像のクリックで拡大表示]
形式検証ツール「SLAM」をWindows Vistaのデバイス・ドライバに適用
形式検証ツール「SLAM」をWindows Vistaのデバイス・ドライバに適用
[画像のクリックで拡大表示]
Microsoft Surfaceを発展させた「Second Light」
Microsoft Surfaceを発展させた「Second Light」
[画像のクリックで拡大表示]
子供向けのプログラミング環境「Boku」も紹介された
子供向けのプログラミング環境「Boku」も紹介された
[画像のクリックで拡大表示]

 米Microsoft Corp.の基礎研究所であるMicrosoft Research担当のSenior Vice PresidentであるRick Rashid氏は,2008年10月27~30日に米Los Angelesで開催されている「Professional Developers Conference 2008(PDC 2008)」の基調講演で,2020年を見据えた研究内容について紹介した。

 ソフトウエア開発者を対象とするPDC 2008の聴衆を意識してか,最初に紹介したのがソフトウエアの形式検証技術を応用した「SLAM」と「Terminator」である。SLAMはC言語で書かれたコードを変更せずに,正しさを検証するツール。APIの呼び出し方などのルールは「SLIC」と呼ぶ独自の言語で記述しておく。Cプログラムから自動的に抽象度を高めたモデルを生成し,SLICで記述した動作と合致するかどうかを検証する。既に「Windows Vista」のデバイス・ドライバの正当性検証に使われている。

 もう一つのTerminatorは,プログラムの停止/生存を証明するためのツール。本来プログラムが正しいかどうかを,実行せずに完全に証明することはできない(チューリングの「停止問題」)。これをいくつか仮定を導入することで,近似的に十分な証明を果たそうというものである。3万5000行のWindowsのデバイス・ドライバに適用して成功したという。

 またマルチタッチのユーザー・インタフェースを用いたテーブル型の操作環境「Microsoft Surface」を発展させたものとして,「Second Light」も紹介した。Second Lightは二つの光源を持つ。テーブルの上にトレーシング・ペーパーなど半透明の物質をかざすと,テーブルの表面とは異なる別の画像を映し出す。例えば地図をテーブルの上に表示しておき,その上にペーパーをかざすとそこには衛星写真が重ねて写るといったことが可能になる。

 このほか,教育目的のプログラミング環境の「Boku」や「World Wide Telescope」なども紹介された。