Filter-Based Methods: After the universal environments are generated, they are combined with the code of the unit and then a model checker such as JPF can be used to verify unit properties (e.g., that there are no runtime exceptions). In many cases, behavioral information about unit interfaces, rather than just signatures, can be exploited to refine the definition of the environment used to complete the unit’s definition. For example, calling remove on an empty set raises a runtime exception. However, the developer of IntSet may know that the set is always used in a context in which remove is called only on a non-empty set. In this case, he or she may want to encode this assumption about the calling context directly into the environment model:
Here, the modeling primitive assume(cond) is used to instruct the underlying model checker to backtrack if cond is not true (in JPF: Verify.ignoreIf(!cond)). Checking the set implementation with this refined environment will yield no runtime exceptions.