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
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.