令和6年度 春期 午前Ⅱ 問23

✓ これが正解エ明確で厳密な意味を定義することができる言語を用いてソフトウェアの仕様を記述して，満たすべき性質と仕様とが整合しているかどうかを論理的に検証する。

解説

形式手法は、厳密な言語で仕様を書き、論理的に検証します。

形式手法は、数学的に厳密な意味をもつ言語を使ってソフトウェアの仕様を記述し、その仕様が満たすべき性質と整合しているかを論理的に確かめる方法です。自然言語で書いた仕様は読み手によって解釈が分かれることがありますが、厳密な言語で書けば曖昧さがなくなり、証明やモデル検査といった手段で矛盾や漏れを機械的に調べられます。人の目で読む方法や、プログラムを動かして確かめる方法とは、検証の考え方が異なります。見分ける軸は、厳密な言語で記述することと、論理的に検証することの二つです。

ほかの選択肢はなぜ違うのか

• ア進行役（モデレーター），記録役などの役割…：進行役や記録役などの役割を決めた複数人で成果物の欠陥を探すのは、インスペクションというレビュー手法の説明です。人の目で確かめる方法で、数学的な裏付けによる検証ではありません。
• イプログラムの内部構造とは無関係に，プログ…：内部構造と無関係に、仕様どおりに機能するかを確かめるのは、ブラックボックステストの説明です。入力と出力を見て確かめる、プログラムを実行する検証方法です。
• ウプログラムの内部構造に着目し，プログラム…：内部構造に着目して、仕様どおりに動作するかを確かめるのは、ホワイトボックステストの説明です。命令や分岐がすべて通るようにテストケースを作り、実行して確かめる方法です。