| abstract | 集合論・論理・代数学などの数学を基礎にした形式手法は，形式仕様記述技術・仕様を詳細化する技術・形式検証から構成され，システム開発の上流工程の段階で曖昧さを排除し，システムで実現すべき機能や制約を厳密に記述することで設計や実装工程へ仕様を正確に伝えるというメリットある．形式手法は効果的ではあるが，導入教育に時間がかかることや極めて高い専門知識が要求されるため現実的にはソフトウェア開発に適用することは難しいのも事実である．本稿では，具体的なアプリケーションの開発を例にとり，形式仕様記述技術と段階的詳細化技術を使い，あらかじめデータやオブジェクトの型の宣言を明確にすることで, 操作に関する形式仕様を書きやすくする方法について一例をあげている．
|
| keywords | 形式仕様，段階的詳細化， |