形式仕様記述

出典: フリー百科事典『ウィキペディア（Wikipedia）』

形式仕様記述（けいしきしようきじゅつ、Formal Specification）とは、ソフトウェアやハードウェアの実装を開発する際に使用される数学的記述。システムが何をすべきかを記述するものであり、どのように実装すべきかを記述する必要はない。そのような仕様を与えることにより、対象システムが仕様に照らして正しいかどうかを形式的検証技法で判定することが可能となる。システム設計の問題点を早期に検出することが可能となり、実装工程に移って多大な出費をした後の後戻りを防ぐという利点がある。他の手法として建築に使われている方法があり、仕様から設計、設計から実装へと段階的に検証可能なステップを踏んで詳細化させていく方法である。

設計（や実装）の「正当性」は単独では宣言できないという点は重要である。正当性は与えられた仕様に照らして初めて検証可能である。形式仕様記述が解決すべき問題を正しく記述できるかどうかは別の問題である。これもまた困難な問題であり、非形式的な実際の問題を抽象化された形式的仕様記述で正しく記述する問題に帰着する。そして、そのような抽象化は形式的証明が不可能である。しかし、仕様が表現することを期待されている特性に関わる定理を証明することによって仕様記述を検証することは可能である。もし正しければ、それらの定理は仕様記述者の仕様記述および根底にある問題領域との関係への理解を深める。正しくない場合、その仕様は元となっている問題領域を正しく反映しているとは言えないので、仕様記述者はさらに理解を深めて仕様記述を改訂することになるだろう。

Z記法は主要な仕様記述言語の1つである。他にも、VDMによるVDM-SL、B-Methodによる Abstract Machine Notation (AMN) などがある。