Pluss, un langage pour le développement de spécifications algébriques modulaires
Institution:
Paris 11Disciplines:
Directors:
Abstract EN:
In this thesis we describe the Pluss specification language. With the Pluss language, it is possible to express both modular algebraic specifications and the development process of such specifications by stepwise refinements. Indeed one of the main originality of Pluss is to state a careful distinction between completed specification components (those that are ready to be implemented) and specification components under development. We study how far some crucial concerns about software development, such as modularity and reusability, can be modelized at the level of the semantics of the specification language. We show that neither the initial approach nor the loose one is powerful enough to reflect our intuition and needs about software modularity and reusability, and we introduce a more sophisticated framework, the stratified loose semantics, which is used to define the formal semantics of the Pluss specification language. The description of the Pluss language is illustrated by numerous examples and a case study, the specification of a subset of the Unix file system.
Abstract FR:
Nous décrivons dans cette thèse le langage de spécification Pluss, qui est un langage permettant d'exprimer des spécifications algébriques modulaires et le processus permettant d'obtenir de telles spécifications par raffinements successifs. Une des principales originalités du langage Pluss est de distinguer entre spécifications achevées (celles qui sont prêtes à être implémentées) et spécifications en cours de développement. Nous étudions dans quelle mesure deux concepts clés en matière de développement de logiciels, la modularité et la réutilisation, peuvent être modélisés de façon adéquate au niveau de la sémantique du langage de spécification. Nous montrons que ni l'approche de type "modèle initial" ni l'approche de type "classe de modèles" ne sont suffisament puissantes, et nous définissons une nouvelle approche, qualifiée d'approche de type"classe stratifiée de modèles", qui est utilisée pour définir la sémantique du langage de spécification Pluss. La description du langage Pluss est illustrée de nombreux exemples et d'une étude de cas, la spécification d'un sous-ensemble du système de gestion de fichiers d'Unix.