In abstract interpretation, the choice of an abstract domain fixes a limit on the precision of the inductive invariants that one can express; however, for a given abstract domain A, there is a most-precise (``strongest'', ...