Validating software specifications against user claims

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. 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