形式仕様

ウィキペディア

形式仕様記述

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/10/03 08:17 UTC 版)

形式仕様記述（けいしきしようきじゅつ、英: formal specification）とは形式手法のひとつで、何らのシステムなどについて、その性質などの仕様を形式的に記述する手法や、そういった手法による仕様の記述である。

形式的な仕様を与えることにより、対象システムが仕様に照らして正しいかどうかを形式的に判定することが可能となる(形式的検証)。また、仕様策定の工程で仕様の不整合を検出することが可能となり、実装工程のような開発の後半での仕様不備発覚、それに伴う手戻り(多大なコストを要する場合が多い)を防ぐという利点がある。他の使われ方として、仕様から設計、設計から実装へと段階的に検証可能なステップを踏んで詳細化し、開発工程で不具合を作りこむのを防ぐ。

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

関連項目

• 形式手法
• ソフトウェア工学
• 仕様記述言語

外部リンク

• A Case for Formal Specification (Technology) by Coryoth 2005-07-30
• Formal Specification

ウィキペディア小見出し辞書

形式仕様

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/05/08 06:08 UTC 版)

「仕様」の記事における「形式仕様」の解説

詳細は「形式仕様記述」を参照 形式仕様は、ソフトウェアやハードウェアを数学的に記述したもので、何らかの実装の開発に使われる。それはシステムが何をすべきかを記述したもので、それをどう実現するかは記述する必要はない。システムの設計が形式仕様に照らして正しいかどうかの形式的検証に使われたりする。これには、工程が先に進む前に正しくない設計を改良できるという利点がある。代替手法としては、仕様から設計への変換、および特に実際の実装への変換に際して、詳細化を行う手法がある。