LIP6 2004/001
- Rapports de recherche
Vers une définition formelle du langage Foc - S. Fechter, C. Dubois
- 59 pages - 04/05/2004- document en - http://www.lip6.fr/lip6/reports/2004/lip6.2004.001.pdf - 462 Ko
- Contact : stephane.fechter (at) nulllip6.fr
- Ancien Thème : SPI
- Mots clés : traits orientés objets, héritage, encapsulation, système de types, espèces, collections, type support
- Directeur de la publication : David.Massot (at) nulllip6.fr
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.
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.