About: 仕様記述言語

仕様記述言語（しようきじゅつげんご）は、システムなどの仕様を記述する、コンピュータ言語（すなわち形式言語）である。形式的でない仕様記述もあるが（後述）、そういったものを含めて何らかの主張がされている場合もある。 プログラミング言語がシステムそのものに変換されるのに対し、仕様記述言語は必ずしもシステムに自動変換されるものではなく、あくまで仕様の妥当性を検証することに重きを置いている。ソフトウェア工学における一般的な設計プロセスの位置づけから、多くはプログラミング言語を記述する前段階に記述されることを期待している。 仕様記述と検証の方法について説明する。仕様記述では、何らかのシステムの仕様を論理学的あるいは代数学的に、形式的に記述する（形式仕様記述）。検証では、論理学や代数学に基づき（すなわち「機械的」に）、無矛盾性などといったシステムにおける「好ましい性質」の保証、あるいはデッドロックの可能性があるといった「好ましくない性質」の不存在を保証する（あるいは存在することを示し、修正を促す）。代表的な形式的仕様記述言語としてZ言語やなどがある。研究段階では長い歴史を持つが、記述が複雑で高度なスキルを要求する上、システム全体の仕様を全て表現するには膨大な量の記述が必要になる。