形式手法による仕様の論理的検証

形式手法では,厳密な意味をもつ形式言語で仕様を記述し,満たすべき性質との整合性を論理的に検証する。 役割を決めた複数人による成果物レビューはインスペクションである。 内部構造を見ずに入出力から確認するのはブラックボックステストである。 プログラム内部構造に着目するのはホワイトボックステストである。

ソフトウェアの品質を確保するための検証に形式手法を用いる。このとき行う検証方法の説明として,適切なものはどれか。

出典令和6年度 春期 情報処理安全確保支援士試験 午前Ⅱ 問23
進行役(モデレーター),記録役などの役割を決めた複数人で,成果物に欠陥がないかどうかを検証する。
プログラムの内部構造とは無関係に,プログラムが仕様どおりに機能するかどうかを検証する。
プログラムの内部構造に着目し,プログラムが仕様どおりに動作するかどうかを検証する。
明確で厳密な意味を定義することができる言語を用いてソフトウェアの仕様を記述して,満たすべき性質と仕様とが整合しているかどうかを論理的に検証する。