仕様記述言語
出典: フリー百科事典『ウィキペディア（Wikipedia）』
仕様記述言語（しようきじゅつげんご）とは、コンピュータを使ったシステム、特にソフトウェアを設計・構築する際に、その仕様を記述するために用いられる言語である。コンピュータ言語の1種である。
プログラミング言語がシステムそのものに変換されるのに対し、仕様記述言語は一般的にシステムに自動変換されることはなく、あくまで仕様の妥当性を検証することに重きを置いている。ソフトウェア工学における一般的な設計プロセスの位置づけから、多くはプログラミング言語を記述する前段階に記述されることを期待している。
仕様記述言語を使った検証の方法は様々である。1つは論理学的あるいは代数学的に記述し、仕様の無矛盾性を保証するものである（形式的仕様記述）。狭義には、仕様記述言語とはこのような形式言語の形態を取る。代表的な形式的仕様記述言語としてZ言語やLOTOSなどがある。研究段階では長い歴史を持つが、記述が複雑で高度なスキルを要求する上、システム全体の仕様を全て表現するには膨大な量の記述が必要になるため、実用上はあまり普及していない。
完全な妥当性は保証できないが、シミュレーションを行うことで、ある限られた場合においての動作を模擬して確かめる方法を採用しているものもある。SpecCはこの立場を取る。また狭義の言語ではないが、RADを使ったプロトタイピングもこの範疇にあると言える。
もう1つは、あくまでシステム全体のモデリングに重きを置き、仕様に対する人間の理解容易性を向上させることで、設計者自身によって（あるいは設計者同士のコミュニケーションによって）妥当性を検討させるものである。UMLなどのモデリング言語がこれに該当する。
