Checking Specifications

Verification is only as good as the specifications. Bugs in specifications can prevent the Prover from detecting bugs in the contracts. This chapter describes tools that you can use to help find bugs in your specifications.

Contents

• Rule Sanity Checks
  • Vacuity checks
  • Assert tautology checks
  • Trivial invariant checks
  • Assertion structure checks
  • Redundant require checks
• Coverage Info
  • Examples
  • Basic vs. advanced mode
  • Completeness
• Bug Injection
• Mutation Testing