Diagrammatic specifications
Dominique Duval · Mathematical Structures in Computer Science · 2003
This paper presents a simple and powerful diagrammatic framework for dealing with specifications in computer science. Following a classical line, we define diagrammatic specifications as a kind of generalised sketch. In addition, the specifications themselves are defined as the realisations of projective sketches. This meta level provides adjunction properties: this is due to a well-known result of Ehresmann. Moreover, we prove in this paper that this meta level also provides an efficient definition of deduction. This work results from a collaboration with Christian Lair.