Towards a formal definition of the Foc language
Vers une définition formelle du langage Foc
Résumé
The Foc project develops a formal language to implement certified components called collections. These collections are specified and implemented step by step: the programmer describes formally the properties of the algorithms, the context in which they are executed, the data representation and proves formally that the implemented algorithms satisfies the specified properties. This programming paradigm implies the use of classic oriented-object features and the use of module features like interfaces and encapsulation of data representation. In this paper we formalize a kernel of the focLanguage language whose main ingredients are multiple inheritance, late binding, overriding, interfaces and encapsulation of the data representation. We specify formally the semantics, the type system, the soundness of the typing discipline.
Le projet Foc développe un langage formel pour implanter des composants certifiés appelés collections. Ces
collections sont spécifiées et implantées pas à pas : le programmeur décrit formellement les propriétés des
algorithmes, le contexte dans lequel ils sont exécutés, la représentation des données et prouve formellement que les algorithmes implantés satisfont les propriétés spécifiées. Ce paradigme de programmation implique
l'utilisation de traits orientés objets classiques et l'utilisation de certain traits des modules comme les interfaces et l'encapsulation de la représentation des données. Dans ce papier on formalise un noyau du langage Foc dont les ingrédients principaux sont le multi-héritage, la liaison retardée, les interfaces et l'encapsulation de la représentation des données. On spécifie formellement la sémantique, le système de type, la sûreté du typage.
| Origine | Fichiers produits par l'(les) auteur(s) |
|---|