Develops a methodology to verify the completeness of formal specification intended for a black-box reuse. Identifies the algorithm to apply the methodology semi-automatically with the help of Larch Theorem Prover.