Ph.D
Group : Verification of Algorithms, Languages and Systems
Constructing Semantically Sound Object-Logics for UML/OCL Based Domain-Specific Languages
Starts on 01/02/2013
Advisor : WOLFF, Burkhart
[Delphine LONGUET]
Funding : Autre financement à préciser
Affiliation : Université Paris-Saclay
Laboratory : LRI
Defended on 06/04/2016, committee :
Directeur de thèse :
M. Burkhart WOLFF
Examinateurs :
M. Achim D. BRUCKER
M. Stéphane MAAG
M. Safouan TAHA
Rapporteurs :
Mme Catherine DUBOIS
M. Bernhard RUMPE
Research activities :
- Formalisation of (Specification and Programming) Languages in Proof Assistants
- Formal Model-Based Testing
Abstract :
Object-based and object-oriented specification languages (like
UML/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 emph{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 emph{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 emph{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 emph{fairly
efficient code}, or emph{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 emph{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
emph{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:
inlineocl{invalid} (exception) and inlineocl{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.
