Validating Software Specifications against User Claims Validating Software Specifications against User Claims Chia-Chu Chiang Viasoft Incorporated Joseph E. Urban Arizona State University Testing provides a way of detecting specification errors. However, testing only shows the presence of errors, but never shows the absence of errors.
Proofs complement the limitations of testing.
Unfortunately, proofs have been considered impractical for showing the correctness. Nevertheless, proofs are highly recommended for critical parts that may risk human life, company finance, or system success. In this paper, a formal specification language is introduced to facilitate proofs of correctness. With theorem proving, a specification is validated against the user claims which may only be concerned about the critical parts of the specification. The answer extraction process explains how and why the specification satisfies the user claims or not.