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. / Object-based and object-oriented specification languages (likeUML/OCL, JML, Spec#, or Eiffel) allow for the creation and destruction, casting and test for dynamic types of statically typed objects. On this basis, class invariants and operation contracts can be expressed; the latter represent the key elements of object-oriented specifications. A formal semantics of object-oriented data structures is complex: imprecise descriptions can often imply different interpretations in resulting tools. In this thesis we demonstrate how to turn a modern proof environment into a meta-tool for definition and analysis of formal semantics of object-oriented specification languages. Given a representation of a particular language embedded in Isabelle/HOL, we build for this language an extended Isabelle environment by using a particular method of code generation, which actually involves several variants of code generation. The result supports the asynchronous editing, type-checking, and formal deduction activities, all "inherited" from Isabelle. Following this method, we obtain an object-oriented modelling tool for textual UML/OCL. We also integrate certain idioms not necessarily present in UML/OCL --- in other words, we develop support for domain-specific dialects of UML/OCL. As a meta construction, we define a meta-model of a part of UML/OCL in HOL, a meta-model of a part of the Isabelle API in HOL, and a translation function between both in HOL. The meta-tool will then exploit two kinds of code generation to produce either fairly efficient code, or fairly readable code. Thus, this provides two animation modes to inspect in more detail the semantics of a language being embedded: by loading at a native speed its semantics, or just delay at another "meta"-level the previous experimentation for another type-checking time in Isabelle, be it for performance, testing or prototyping reasons. Note that generating "fairly efficient code", and "fairly readable code" include the generation of tactic code that proves a collection of theorems forming an object-oriented datatype theory from a denotational model: given a UML/OCL class model, the proof of the relevant properties for casts, type-tests, constructors and selectors are automatically processed. This functionality is similar to the datatype theory packages in other provers of the HOL family, except that some motivations have conducted the present work to program high-level tactics in HOL itself. This work takes into account the most recent developments of the UML/OCL 2.5 standard. Therefore, all UML/OCL types including the logic types distinguish two different exception elements: invalid (exception) and null (non-existing element). This has far-reaching consequences on both the logical and algebraic properties of object-oriented data structures resulting from class models. Since our construction is reduced to a sequence of conservative theory extensions, the approach can guarantee logical soundness for the entire considered language, and provides a methodology to soundly extend domain-specific languages.
| Identifer | oai:union.ndltd.org:theses.fr/2016SACLS085 |
| Date | 06 April 2016 |
| Creators | Tuong, Frédéric |
| Contributors | Université Paris-Saclay (ComUE), Wolff, Burkhart |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text, Image, StillImage |
Page generated in 0.0022 seconds