Discharging Assumptions

Question

Explain the term Discharging Assumptions in Program Model Checking?

Answer 1

Environment assumptions (or filters) capture the knowledge about the usage of software units and they help to refine a naively generated environment. These assumptions need to be subsequently checked against implementations of the missing components (that represent the environment) in order to make sure that the entire system satisfies the desired properties. For example, you need to check assert(!empty()) whenever remove is invoked by a client application that uses IntSet.

Assumptions can be encoded in a variety of forms, such as predicates (!empty(), in the set example), finite-state machines, temporal logical formulas, or regular expressions that encode patterns of component operations that the environment may execute.

Checking component property (P) under environment assumptions (A) forms the assume guarantee paradigm, and it is the basis of many formal frameworks for modular verification (Jones 1983; Pnueli 1984): P is the guarantee that the component provides under assumption A. When A and P are temporal logical formulas, then it is possible to model check directly A => P on the unit closed with the universal environment; here “=>” denotes logical implication: P is checked only on the behaviors that satisfy (i.e., are
filtered by) A. Alternatively, as discussed for the set example, you can encode the assumptions directly into the environment (in which case A is eliminated from the formula to be model checked).

Regular expressions are a familiar formal notation to many developers, and often easier to use than temporal logics for specifying environment assumptions. Regular expressions defined over the alphabet of unit operations describe a language of operations that can be initiated by the environment. As an example, java.util.Iterator presents a standard interface for generating the elements stored in a Java container such as a set. This interface assumes that for each instance i of a class implementing the Iterator, all client applications will call methods in an order that is consistent with the following regular expression assumption:

(i.hasNext; i.next(); i.remove()?)*

This expression encodes sequencing (a call to hasNext() must precede a call to next(), otherwise a runtime exception may be thrown if the iteration has no more elements) and also optional calls (remove()) that can be repeated 0 or more times (*). This assumption can be easily translated into code to encode a driver or the Iterator, or into an LTL formula that can then be used to be discharged with SPIN.