On collecting semantics for program analysis

Reasoning on a complex system in the abstract interpretation theory starts with a formal description of the system behavior specified by a collecting semantics. We take the common point of view that a collecting semantics is a very precise semantics from which other abstractions may be derived. We elaborate on both the concepts of precision and derivability, and introduce a notion of adequacy which tell us when a collecting semantics is a good choice for a given family of abstractions. We instantiate this approach to the case of first-order functional programs by considering three common collecting semantics and some abstract properties of functions. We study their relative precision and give a constructive characterization of the classes of abstractions which are adequate for the collecting semantics.