Constructing Semantically Sound Object-Logics for UML/OCL Based Domain-Specific Languages

Construction de Logiques-Objet Sémantiquement Correct pour des Langages à Domaines Spécifiques Basés sur UML/OCL Les langages de spécifications basés et orientés objets (comme UML/OCL, JML, Spec#, ou Eiffel) permettent la création et destruction, la conversion et tests de types dynamiques d'objets statiquement typés. Par dessus, les invariants de classes et les opérations de contrat peuvent y être exprimés; ces derniers représentent les éléments clés des spécifications orientées objets. Une sémantique formelle des structures de données orientées objets est complexe : des descriptions imprécises mènent souvent à différentes interprétations dans les outils qui en résultent. Dans cette thèse, nous démontrons comment dériver un environnement de preuves moderne comme un méta-outil pour la définition et l'analyse de sémantique formelle de langages de spécifications orientés objets. Étant donné une représentation d'un langage particulier plongé en Isabelle/HOL, nous construisons pour ce langage un environnement étendu d'Isabelle, à travers une méthode de génération de code particulière, qui implique notamment plusieurs variantes de génération de code. Le résultat supporte l'édition asynchrone, la vérification de types, et les activités de déduction formelle, tous "hérités" d'Isabelle. En application de cette méthode, nous obtenons un outil de modélisation orienté objet pour du UML/OCL textuel. Nous intégrons également des idiomes non nécessairement présent dans UML/OCL --- en d'autres termes, nous développons un support pour des dialectes d'UML/OCL à domaine spécifique. En tant que construction méta, nous définissons un méta-modèle d'une partie d'UML/OCL en HOL, un méta-modèle d'une partie de l'API d'Isabelle en HOL, et une fonction de traduction entre eux en HOL. Le méta-outil va alors exploiter deux procédés de générations de code pour produire soit du code raisonnablement efficace, soit du code raisonnablement lisible. Cela fournit donc deux modes d'animations pour inspecter plus en détail la sémantique d'un langage venant d'être plongé : en chargeant à vitesse réelle sa sémantique, ou simplement en retardant à un autre niveau "méta" l'expérimentation précédente pour un futur instant de typage en Isabelle, que ce soit pour des raisons de performances, de tests ou de prototypages. Remarquons que la génération de "code raisonnablement efficace", et de "code raisonnablement lisible" incluent la génération de code tactiques qui prouvent une collection de théorèmes formant une théorie de types de données orientés objets d'un modèle dénotationnel : étant donné un modèle de classe UML/OCL, les preuves des propriétés pertinentes aux conversions, tests de types, constructeurs et sélecteurs sont traitées automatiquement. Cette fonctionnalité est similaire aux paquets de théories de types de données présents au sein d'autres prouveurs de la famille HOL, à l'exception que certaines motivations ont conduit ce travail présent à programmer des tactiques haut-niveaux en HOL lui-même. Ce travail prend en compte les plus récentes avancées du standard d'UML/OCL 2.5. Par conséquent, tous les types UML/OCL ainsi que les types logiques distinguent deux éléments d'exception différents : invalid (exception) et null (élément non-existant). Cela entraîne des conséquences sur les propriétés aussi bien logiques qu'algébriques des structures orientées objets résultant des modèles de classes. Étant donné que notre construction est réduite à une séquence d'extension conservative de théorie, notre approche peut garantir la correction logique du langage entier considéré, et fournit une méthodologie pour étendre formellement des langages à domaine spécifique.