Type Vacuity Checking - lgwagner/SpeAR GitHub Wiki

If a specification uses predicate subtypes, one must be sure the defined type is not vacuous. A vacuous predicate subtype has no satisfying values.

The following example shows a specification that defines two types. The first type posnat defines a type that is always greater than 0. The second type vacuous defines a new type that uses posnatas its base type, and further restricts its values to all values that are less than 0. By inspection one can tell that there is no integer that is both positive and negative simultaneously.

SpeAR provides a type vacuity analysis that uses model checking to determine if there are no values that satisfy the specified type. This can be access by right-clicking on the type definition and choosing Check Type Validity from the drop down menu. This process is shown below in the following image.