Rapport de recherche n° 2000-04

Auteur : Dominique Duval & Christian Lair

Second part: Mosaics for Implicit Specification

Nbre de pages : 60

Documents : Article (PDF)

Abstract: SKETCHES AND SPECIFICATIONS is a common denomination for several papers which deal with applications of Ehresmann's sketch theory to computer science. These papers can be considered as the first steps towards a unified theory for software engineering. However, their aim is not to advocate a unification of computer languages; they are designed to build a frame for the study of notions which arise from several areas in computer science.

These papers are arranged in two complementary families:


The reference manual provides general definitions and results, with comprehensive proofs. On the other hand, the user's guide places emphasis on motivations and gives a detailed description of several examples. These two families, though complementary, can be read independently. No prerequisite is assumed; however, it can prove helpful to be familiar either with specification techniques in computer science or with category theory in mathematics.

These papers are under development, they are, or will be, available at: http://www.unilim.fr/laco/rapports.

In addition, further papers about APPLICATIONS are in progress, with several co-authors. They deal with various topics, including the notion of state in computer science, overloading, coercions and subsorts.

These articles owe a great deal to the working group sketches and computer algebra; we would like to thank its participants, specially Catherine Oriat and Jean-Claude Reynaud, as well as the CNRS.

These papers have been processed with LATEX and XY-pic.

Second Part: Mosaics for Implicit Specification

The aim of this paper is to introduce new specifications, more powerful than wefts. These new specifications are called mosaics. They generalize wefts, in order to be able to deal with implicit features of computer languages. In addition, each mosaic can be explicited, by building a weft with the same meaning. This construction is called the ribbon product, it is related to the family of tensor products.

This paper is part of a general study of some applications of Ehresmann's sketch theory to computer science, along with the reference manual. The only prerequisite to read this article is the first part of this user's guide. Here, as well as in the first part, we focus on the interpretations of our specifications. The point of view of programs and computation will be studied later.

Retour à la liste des rapports