Data Independence: A system is data independent if the values of the infinite program data it manipulates are not relevant to the behavior of the system—for example, a protocol that transmits messages may be proved correct regardless of the contents of the messages that are transmitted. It has been shown (Wolper 1985) that reasoning about pair-wise message ordering properties over a communication channel that accepts large domains of values can be achieved by using an abstract domain of size three. Note that this kind of reasoning is possible only when the values that are passed through the channel are not modified or tested by the program (i.e., the program is data independent). The three-valued abstract domain {d1, d2, other} provides the ability to distinguish between two concrete elements, but it abstracts from their values. Such an abstraction can be thought of as a “symbolic” Set abstraction, where d1 and d2 are placeholder for any two different values of a particular concrete data domain, while all the other values are abstracted to other.