プログラムの構造的統合

プログラムの構造的合成(SSP) は、命題計算に基づく(自動)プログラム合成の特殊な形式です。より正確には、直観主義論理を使用してプログラムの構造を詳細に記述し、サブルーチンやコンピュータ コマンドなどの部分からプログラムを自動的に構成できるようにします。これらの部分は正しく実装されていると想定されているため、これらの部分の正しさの検証は必要ありません。SSP は、サービス指向アーキテクチャのサービスの自動構成^[1]や、大規模なシミュレーションプログラムの合成に適しています。^{[2] [3]}

自動プログラム合成は人工知能の分野で始まり、自動問題解決を目的としたソフトウェアが登場しました。最初のプログラム合成装置は1969年にコーデル・グリーンによって開発されました。 ^[4]ほぼ同じ時期に、R.コンスタブル、Z.マンナ、R.ウォルディンガーなどの数学者が、自動プログラム合成に形式論理を利用できる可能性を説明しました。実際に適用可能なプログラム合成装置が登場したのは、かなり後のことでした。

プログラムの構造的合成というアイデアは、 1979年にアンドレイ・エルショフとドナルド・クヌースが主催した現代数学とコンピュータサイエンスのアルゴリズムに関する会議^{[5]で発表されました。このアイデアは、} G.ポリアの有名な問題解決に関する本^[6]に由来しています。SSPで問題を解決するための計画を立てる方法は、形式システムとして提示されました。システムの推論規則は、1982年にG.ミンツとE.チュグ^[7]によって論理的に再構成され、正当化されました。SSPを使用するプログラミングツールPRIZ ^[8]は、1980年代に開発されました。

SSPをサポートする最近の統合開発環境としては、ドメイン固有言語を実装し、大規模なJavaプログラムを開発するためのモデルベースのソフトウェア開発プラットフォームであるCoCoViLa ^[9]がある。

プログラムの構造的合成は、関数とみなすことができる、すでに実装されているコンポーネント（コンピュータコマンドやソフトウェアオブジェクトメソッドなど）からプログラムを構成する方法です。合成の仕様は、直観主義命題論理で、関数の適用可能性に関する公理を記述することによって与えられます。関数fの適用可能性に関する公理は、論理的含意です。

X ₁ ∧ X ₂ ∧ ... ∧ X _m → Y ₁ ∧ Y ₂ ... Y _n、

ここで、X ₁、X ₂、... X _{m は}関数fの適用の前提条件であり、Y ₁、Y ₂、... Y _{n は}関数 f の適用の事後条件です。直観主義論理では、関数f はこの式の実現と呼ばれます。前提条件は、入力データが存在することを述べる命題である場合があります。たとえば、X _{i は}「変数x _{i が}値を受け取った」 という意味を持ちますが、関数f を使用するために必要なリソースが利用可能であるなど、他の条件を示す場合もあります。前提条件は、上記の公理と同じ形式の含意である場合もあります。その場合はサブタスクと呼ばれます。サブタスクは、関数fが適用されたときに入力として利用可能でなければならない関数を示します。この関数自体は、SSP のプロセスで合成されなければなりません。この場合、公理の実現は高階関数、つまり別の関数を入力として使用する関数です。たとえば、式

(状態 →次の状態) ∧初期状態→結果

2 つの入力と出力result を持つ高階関数を指定できます。最初の入力は、状態からnextState を計算するために合成される関数で、2 番目の入力はinitialStateです。高階関数により SSP に一般性が与えられます。つまり、合成されたプログラムに必要な制御構造はすべて事前にプログラムしておき、それぞれの仕様で自動的に使用できます。特に、ここで提示される最後の公理は、複雑なプログラムの仕様、つまりシステムの状態からnextState を計算できるモデル上で動的システムをシミュレートするためのシミュレーション エンジンです。

• 自動ソフトウェアエンジニアリングホームページ