Loading article…
仕様言語は、システム分析、要件分析、システム設計の際に使用されるコンピュータ科学の形式言語であり、システムの実行可能コードを生成するために使用されるプログラミング言語よりもはるかに高いレベルでシステムを記述するために使用されます。[ 1 ]
仕様言語は一般的に直接実行されるものではありません。仕様言語は、何をするかを記述するためのものであり、どのように行うかを記述するためのものではありません。[ 2 ]要求仕様が不必要な実装の詳細で煩雑になっている場合は、エラーとみなされます。
多くの仕様記述手法に共通する基本的な前提は、プログラムを、データ値の集合とそれらの集合に対する関数を含む代数的またはモデル理論的な構造としてモデル化するという点である。このレベルの抽象化は、プログラムの入出力動作の正しさが他のすべての特性よりも優先されるという考え方と一致する。
特性指向型の仕様記述アプローチ（例えばCASLが採用している）では、プログラムの仕様は主に論理公理から構成され、通常は等価性が重要な役割を果たす論理体系において、関数が満たすべき特性を、多くの場合、関数間の関係性のみによって記述します。これは、 VDMやZ記法などのフレームワークにおける、いわゆるモデル指向型の仕様記述とは対照的です。モデル指向型の仕様記述は、要求される動作の単純な実現から構成されます。
仕様は、実際に実装される前に、洗練プロセス（実装の詳細を詰めるプロセス）を経る必要があります。このような洗練プロセスの結果として得られるのが実行可能なアルゴリズムであり、これはプログラミング言語で記述されるか、あるいは対象となる仕様言語の実行可能なサブセットで記述されます。例えば、ハルトマンパイプラインは、適切に適用すれば、直接実行可能なデータフロー仕様とみなすことができます。別の例としては、アクターモデルがあります。アクターモデルには特定のアプリケーション内容がなく、実行可能にするためには特殊化する必要があります。
仕様記述言語の重要な用途の一つは、プログラムの正当性の証明を作成することである（定理証明器を参照）。
ウィキメディア・コモンズにある仕様言語関連のメディア