Abstract Parametric Classes and Abstract Data Types defined by Classical and Constructive Logical Methods

We introduce a methodology to treat abstract data types (ADT), abstract parametric classes (APC) and subclasses, together with appropriate inheritance properties, by means of first order theories. The notion of a first order theory axiomatizing an ADT is based on the notion of isoinitial model and has been proposed by the authors in previous papers (Bertoniet al. (1979), Bertoniet al. (1983), Bertoniet al. (1984)). A theory formalizing an APC is seen, in this paper, as a theory T incompletely axiomatizing an ADT. Given a class C of ADTʹs, the class formalized by T can be seen (under suitable soundness conditions on T) as the class of the instances of T over C. An instantiation of T by an ADT I of CcompletesT into a T′ formalizing an ADT I′, which extends I and inherits the properties of the APC T. We use both classical and constructive methods in the following sense: on the one hand, the semantics is based on classical model theory; on the other hand, the soundness of a consistent axiomatization can be analyzed by purely syntactical methods, in terms of provability within suitable constructive systems. A theory T formalizing an APC (or an ADT) is not given by a list of axioms, but by a suitable "APC-expression", which explicitly or implicitly (but effectively ) defines the axioms of T. We have APC-expressions to define APCʹs, to extend already defined APCʹs and to instantiate APCʹs (into ADTʹs or subclasses). We allow also "recurrence APC-expressions". At the end of the paper we give some examples showing how the proposed methodology works.