Istituto di Scienza e Tecnologie dell'Informazione     
Inverardi P., Martini S., Montangero C. Is type checking practical for system configuration?. In: TAPSOFT'89 - International Joint Conference on Theory and Practice of Software Development (Barcelona, Spain, 13-17 March 1989). Proceedings, vol. 2 J. Diaz and F. Orejas (eds.). Springer, 1989.
The paper describes ongoing work on a facet of software specification, namely system configuration, i.e. the specification of the structure of the system and of the operations needed to build it. We want to verify the adequacy of Higher Order Typed Functional Languages (HOTFULs), like Pebble [Lampson&Burstall88], SOL [Mitchell&Plotkin 85] and others [Cardelli 85, Cardelli&Wegner 85], to model the configuration facilities of modern languages for system programming like Ada, Chili and Modula-2: no thorough study has been done in this direction, even if the literature is full of small scale sketches, which are used to claim that such languages are indeed adequate. We are using the new configuration concepts for distributed systems introduced on top of Ada in the Cnet project [Inverardi&Mazzanti&Montangero 85, Cnet 85] as a case study, since they provide a good test bed being an enhancement of Ada advanced configuration facilities. The main result is that checking correctness 01 a Cnet configuration can be reduced to type checking in a suitable HOTFUL. However, the process is nor straightforward enough, so that the question in the title is still open. As a side result, requirements have been assessed for a suitable HOTFUL: definability of (generally) recursive types, availability of the type of all types and of a peculiar inheritance mechanism.

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional