プログラミング科学とは？

プログラミング科学とは？

プログラミング科学が対象とするプログラムは、コンピュータ・プログラミングに限らず、通信手順（communication protocol）、組織における仕事の流れ（business workflow）など、広い意味での情報処理の手順一般です。計算機科学で研究されてきたコンピュータ・プログラミングの数理科学的モデルを、通信手順や仕事の流れにも適用することができます。

• プログラムとは何か？ （算譜意味論）

• 正しいプログラムとは？（算譜検証論）

• システムが妥当だとは？（妥当性確認論）

などがプログラミング科学の基本的な問いです。

算譜意味論

「算譜」はプログラムの訳語です。プログラムや計算過程、制御過程の数学的モデルを研究します。数学的モデルに基づいた計算機言語を設計する計算機言語論も、密接に関連する分野です。

算譜検証論

プログラムが仕様を正しく満たすことを検証する手法やその過程を研究します。コンピュータプログラムの検証理論は、もっと一般のシステムが仕様を満たすことを検証する過程にも適用することができると考えられます。

数理論理学における形式理論とそのモデルの言葉を使うと、形式理論における定理を形式的に証明することや、形式的理論の語彙(signature)に関する「構造」が確かにその形式的理論のモデルになっていることの証明などにあたることをおこなうのが検証です。形式理論が仕様、モデルがプログラムやシステム（いわゆる実装）に当たります。

妥当性確認論

プログラムの仕様が正しい（妥当である）ことを確認する過程を研究します。

数理論理学では形式理論が「正しい」という考えはありませんが、「矛盾していない」(consistent)という考えはあります。妥当性確認では、仕様が矛盾していないことはもちろん要求されますが、それだけでなく、社会常識や法律・規則、などに合っていることも要求されます。

厄介なのは、「こういう条件さえ満たしておれば妥当である」と言い切ってしまうことができないのが、システムの妥当性の本質であることです。システムの妥当性は、その時々の科学水準によって変化しますし、極端な場合、そのときの国の政治体制によってさえ左右されます。だとすると、「これこれであれば妥当だ」という客観的な条件が得られないことは当然といえるでしょう。妥当性には大なり小なり主観的なところがあります。

当研究所におけるプログラミング科学研究

システムの妥当性を確認することによって、システムへのアシュランス、安心が生まれます。妥当性確認の結果だけではなく、そこに至る過程をすべて記した「アシュランスケース」と呼ばれる文書が最近脚光を浴びています。アシュランスケースは通常、数百ページから数千ページに亘る大部の文書ですが、その内容の些細な誤りが大事故に繋がりうるので、文書の整合性に関する精密な検査が必要です。通常、アシュランスケースは日本語で記されますが、これをコンピュータで解析しやすい言語で記し、整合性検査を自動的に行う方法論を当研究所では研究しています。

我々は形式アシュランスケースを記す言語として、プログラミング言語Agdaを用いることにしています。

IPA（（独）情報処理推進機構）からの受託研究プロジェクトFFO (Formal assurance case Framework for Open systems dependability) を進めています。システム工学、ソフトウェア工学やディペンダビリティに関する国際標準の制定活動にも参加しています。