**Auteur : **Dominique Duval & Christian Lair

**Titre : **SKETCHES AND SPECIFICATIONS - USER'S GUIDE

First part: Wefts for Explicit Specifications

**Nbre de pages : **61

**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:

REFERENCE MANUAL and USER'S GUIDE.

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

- REFERENCE MANUAL:
- First Part: Compositive Graphs
- Second Part: Projective Sketches
- Third Part: Models

- USER'S GUIDE:
- First Part: Wefts for Explicit Specification
- Second Part: Mosaics for Implicit Specification
- Third Part: Functional and Imperative Programs

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 L^{A}T_{E}X
and XY-pic.

The aim of this paper is to define *wefts* (for the French
``*trames*'') and to show how they can be used for
specification issues in computer science. Moreover, in subsequent
papers, wefts will be extended to *mosaics*, in order to deal
with implicit features of computer languages, including the notion of
state. Here and in the following paper, we focus on the realizations
of the wefts and mosaics, which give them their meaning. Programs
will be considered later: wefts provide a good frame for functional
programming, while mosaics extends it to imperative programming.

This paper is part of a general study of some applications of Ehresmann's sketch theory to computer science, along with the reference manual. No prerequisite is assumed to read it.

Retour à la liste des rapports