La structure logique des théories sémantiques modulaires des systèmes logiciels

Résumé Cet article étudie la structure des théories sémantiques sur des systèmes computationnels modulaires et applique la théorie algébrique des institutions pour fournir une représentation logique de ces théories. Une théorie sémantique modulaire est ici définie par un ensemble de théories sémantiques, chacune correspondant à un module de programme, et par un ensemble de relations reliant les modèles de différentes théories sémantiques. Une théorie sémantique d'un seul module est fournie en termes de l'ensemble des ∑-modèles mappés depuis la catégorie Th des ∑-théories et générant une hiérarchie de structures allant d'un modèle abstrait à un modèle concret de données. La collection de modèles abstraits représentant différents modules d'un programme est formalisée comme la catégorie des institutions INS, où les morphismes de théorie expriment des raffinements, des intégrations et des compositions entre couples de modules. Enfin, il est requis qu'un morphisme dans INS à tout niveau se produise si et seulement si le même morphisme se produit au niveau inférieur à côté de la hiérarchie Th.