I decided to do some more reading on the site that agumonkey provided. In particular this link, also by Patrick Cousot: https://www.di.ens.fr/~cousot/publicati

I decided to do some more reading on the site that agumonkey provided. In particular this link, also by Patrick Cousot: https://www.di.ens.fr/~cousot/publications.www/Cousot-LNCS2000-sv-sb.pdf https://www.di.ens.fr/~cousot/publications.www/Cousot-LNCS20... [pdf] - Abstract Interpretation Based Formal Methods and Future Challenges, 2000 > All abstractions considered in this paper are “from above” so that the abstract semantics describes a superset or logical consequence of the concrete semantics. Abstractions “from below” are dual and consider a subset of the concrete semantics. An example of approximation “from below” is provided by debugging techniques which consider a subset of the possible program executions or by existential checking where one wants to prove the existence of an execution trace prefix fulfilling some given specification. In order to avoid repeating two times dual concepts and as we do usually, we only consider approximations “from above”, knowing that approximations “from below” can be easily derived by applying the duality principle (as found e.g. in lattice theory). This is where he's getting the "superset" part. The abstraction describes many possible concrete implementations and so is a superset of all of them. Finding a particular concrete implementation or following a particular trace of a particular concrete implementation in a particular environment would be finding a subset (or particular element) of the set. Relatedly, consider the idea of an "abstract data type" like a stack. We can describe a stack's abstract behavior (last in/first out collection with push/pop/peek operations) without describing any particular concrete details or environments. That abstract description is applicable to all stack implementations, though when we get to concrete implementations they may have further restrictions (an array-based stack has a maximum stack depth set at the start if we don't allow reallocation, a linked-list based stack has a size limit as well but it's limited by system memory instead of an initial fixed number, etc.). This ADT of a stack is describing a superset of all concrete implementations in that it is describing something common to all of them. If it were a subset of all concrete implementations then it would only describe the behavior of some concrete implementations of a stack, which means we would have concrete implementations which are not compliant with our abstract notion of stack. That would be odd. In OO or type terms this is a superclass or supertype of all concrete stack implementations, and the actual concrete implementations are subclasses or subtypes of the stack ADT. Subclasses/subtypes are subsets of the superclass or supertype. EDIT: Stacks are last in/first out. Needed coffee to catch that mistake.