Algebraic specification techniques for parametric types with logic-based constraints

摘要

Mainstream object-oriented languages now offer capabilities of generic types with bounded type parameters, but they typically do not provide support for specifying semantic requirements on the type parameters' methods beyond conformance of signatures. Regrettably, even object-oriented assertion languages, such as JML, have nontrivial limitations in this regard. Yet many interesting parameterized types require additional semantic features if they are to function as intended. We illustrate the issues with a case study of project scheduling based on the Project Management Institute's generic characterization of task breakdowns. We consider algebraic techniques for instantiating parametric types in such a way that the semantic requirements expressed by logic-based constraints propagate to the instantiating types. These techniques argue for more general bindings of actual type parameters for the formal ones which do not have the restrictions of current programming languages. We show that types equipped with constraints should be viewed as theories, and the bindings as morphisms of types as theories. We translate these software specifications into theories in the PVS specification language. These proposals lead to conclusions about language features for more general, semantic bindings of the actual for the formal type parameters, at least in the assertion languages.