A generic object-calculus based on Addressed Term Rewriting Systems
Résumé
In a previous paper we have outlined a framework (or a generic object-calculus) called \Obja, for modeling \textit{object calculi}. In this one, we would like to describe the foundations of \Obja{}. This framework is essentially a detailed formal operational semantics of object based languages, in the style of the Lambda Calculus of Objects. As a formalism for specification \Obja{} is arranged in \textit{modules}, permitting a natural classification of many object-based calculi according to their features, including their reduction-strategies. In particular there are modules for calculi of non mutable objects (\ie, \emph{functional object calculi}) and for calculi of mutable objects (\ie, \emph{imperative object calculi}). As a computational formalism \Obja{} is based on rewriting rules. Classical first-order term rewriting systems are not appropriate since we want to reflect aspects of implementation practice such as sharing, cycles in data structures and mutation. Therefore we define the notion of \textit{addressed terms}, and develop the corresponding notion of \textit{addressed term rewriting systems}.
Dans un article précédent, nous avions présenté un cadre de travail (ou si l'on préfère un calcul générique) appelé \Obja, pour modéliser des calculs d'objets, tandis que dans ce rapport, nous voudrions décrire les bases formelles d'\Obja. Ce cadre est essentiellement une sémantique opérationnelle formelle et détaillée des langages d'objets. En temps que formalisme de spécification, \Obja{} est disposé en modules, qui permettent une classification naturelle des divers calculs à objets par rapport à leurs caractéristiques, y compris leurs stratégies de réduction. En particulier, \Obja{} contient des modules qui décrivent les calculs à objets non mutables (c-à-d les \emph{calculs à objets fonctionnels}) et des modules qui décrivent les calculs à objets mutables (c-à-d les \emph{calculs à objets impératifs}). En temps que formalisme de calculs, \Obja{} est fondé sur des règles de réécriture, mais les systèmes de réécriture classiques du premier ordre sont inappropriés, car nous souhaitons refléter des aspects relevant de la pratique des implanteurs tels que le partage, les cycles dans les structures de données et la mutation. Pour cela, nous définissons la notion de terme avec adresses et développons la notion correspondante de système de réécriture avec adresses.
Origine : Fichiers produits par l'(les) auteur(s)