A Framework for Inherent Vacuity

摘要: Vacuity checking is traditionally performed after model has terminated successfully. It ensures that all the elements of specification have played a role in its satisfaction by design. gets as input both design and specification, based on an in-depth investigation relation between them. been proven to be very useful detecting errors modeling or specification. The need check quality specifications even more acute property-based , where only input, serving basis development system. Current work property assurance suggests various sanity checks, mostly satisfiability, non-validity, realizability, but lacks general framework for reasoning about specifications. We describe inherent vacuity which carries theory setting Essentially, inherently vacuous if it can mutated into simpler equivalent we show coincide with fact satisfied vacuously systems. We also study complexity vacuity, conclude while leads better capture designer intent, not complex than simple property-assurance checks.