A Framework for Defining Object-Calculi
Résumé
In this paper, we give a general framework for the foundation of an operational (small step) semantics of object-based languages with an emphasis on functional and imperative issues. The framework allows classifying very naturally object-based calculi according to their main implementation techniques of inheritance, namely "delegation" and "embedding". This distinction comes easily from the choice of the rules we make. Our framework is founded on two previous works, namely the "Lambda Calculus of Objects" of Fischer, Honsell, and Mitchell for the object aspects and the lambda-sigma-w-a of Benaissa, Lang, Lescanne, and Rose for the description of the operational semantics and sharing. The former is the formalization of a small delegation-based language which contains both lambda calculus and object primitives to create, update, and send messages to objects, while the latter is designed to provide a generic description of functional language implementations and is based on a calculus of explicit substitutions extended with addresses to speak about memory management. The framework is presented as a set of "modules", each of which captures a peculiar aspect of object-calculi (functional vs. imperative, delegation vs. embedding, and any combination of them). Our framework satisfies some crucial properties, namely "confluence" on the functional fragment (the final result does not depend on the sequence of computations i.e., on the evaluation strategy), "operational soundness" (our calculi yield the same results on the same data as in the Lambda Calculus of Objects), "subject reduction" (programs preserve types), "type soundness" (a typed program can not go wrong as invoking an unknown method on an object).
Dans cet article, nous définissons un système général pour la fondation d'une sémantique opérationnelle (à pas réduit) des langages basés sur les objets, en insistant sur des problèmes propres aux langages fonctionnels ou impératifs. Dans ce cadre, nous pouvons classifier très naturellement les calculs basés sur les objets selon leur principale technique d'implantation de l'héritage, notamment "délégation" et "emboîtement". Cette distinction est faite simplement dans le choix des règles. Notre système se fonde essentiellement sur deux travaux précédents, le Lambda Calcul des Objets de Fisher, Honsell, et Mitchell pour les aspects objets, et le calcul lambda-sigma-w-a de Benaissa, Lang, Lescanne, et Rose pour la description de la sémantique opérationnelle et du partage. Le premier est la formalisation d'un petit langage basé sur la délégation qui contient à la fois le lambda calcul et des primitives sur les objets permettant de les créer, de les modifier, et de leur envoyer des messages, tandis que le second est conçu pour donner une description générique des langages fonctionnels et est basé sur un calcul de substitution explicite étendu avec des adresses pour modéliser la gestion de la mémoire. Le système est présenté sous la forme d'un ensemble de "modules", chacun décrivant un aspect particulier des calculs à objets (fonctionnel ou impératif, délégation ou emboîtement, et toute combinaison de ceux-ci). Notre système satisfait des propriétés cruciales comme la "confluence" sur le fragment fonctionnel (le résulat final ne dépend pas de la séquence des calculs, c'est-à-dire de la stratégie d'évaluation), la "correction opérationnelle" (nos calculs retournent le même résultat pour les mêmes données que le Lambda Calcul des Objets), l'"auto réduction" (les programmes préservent les types), et la "sûreté du typage'' (un programme typé ne peut pas mener à une erreur d'exécution comme invoquer une méthode inconnue sur un objet).
Origine : Fichiers produits par l'(les) auteur(s)