LIP6 2005/011
- Reports
Une nouvelle extension de ML avec des traits orientés objets de FOCAL - S. Fechter
- 39 pages - 12/20/2005- document en - http://www.lip6.fr/lip6/reports/2005/lip6-2005-011.pdf - 692 Ko
- Contact : stephane.fetcher (at) nulllip6.fr
- Ancien Thème : SPI
- Keywords : object oriented language, certified libraries, semantics, abstraction, type system, type soundness, species, collections, carrier type
- Publisher : Thierry.Lanfroy (at) nulllip6.fr
The FOCAL framework provides a set of tools to build certified libraries. This language provides two constructions: species and collections. A species declares or defines a data representation, namely the carrier, and specifies or implements algorithms working on this data representation. Species construction is realized with object features: multi-inheritance, redefinition, late binding, parameterization by collections. At the top of an hierarchy of species, carrier and functions are declared. At the bottom, carrier and functions are defined and every property is proved.
Such as species is said to be complete. A collection is obtained from a complete species by abstracting its carrier type and definitions. In this paper, we formalize operational aspects of object oriented features of FOCAL.
We present the model FML, an extension of ML with notions of species and collection. We provide a type system, an operational semantics and we prove the type soundness.
Such as species is said to be complete. A collection is obtained from a complete species by abstracting its carrier type and definitions. In this paper, we formalize operational aspects of object oriented features of FOCAL.
We present the model FML, an extension of ML with notions of species and collection. We provide a type system, an operational semantics and we prove the type soundness.