The SETS Calculus Home Page
[ DI/UM ]

The SETS Calculus Project

The SETS Calculus is a data reification calculus developed by the Formal Methods Group of the Informatics Department of Minho University. SETS is based on set-theory and (a modest use of) category theory. It arose in 1987 (see [Ol87] in the Bibliography below) as an attempt to introduce explicit transformational design rules in program data structuring.

Funding

As a research project, SETS started as part of the CAMILA (JNICT Tit 169.90) project, jointly developed by the Informatics Department of Minho University and the INESC R&D Institute, a member of ERCIM . Currently, it is part of the LOGCOMP project.

Past and Present of SETS

SETS finds its earliest motivation in a Ph.D. thesis [Ol84] on transformational dataflow program design. In this work, an underlying formal model of a dataflow architecture (the Manchester tagged dataflow machine) was developed in which data traffic was described and reasoned about in the isomorphism calculus of the category of finite sets.

This reasoning strategy was extended in [Ol87] by introducing set-theoretical inequationl laws capturing the set-theoretical cardinality ordering, up to isomorphism, in the context of final algebra semantics. [Ol90] provided some basic results of the emerging calculus, namely those which make for systematic inference of retrieve functions and data-type invariants in data reification.

The reification style of SETS becomes more apparent in [Ol92], in which SETS is presented as an inequational calculus of functional abstraction invariants. In brief, each law in SETS becomes an inequation of the form A <f,p B meaning that:

• there is an abstraction surjection f from B to A;
• wherever f is a partial function, p is the characteristic predicate defining its domain -- the so-called concrete invariant induced in B;
• in the terminology of the Morgan's Refinement Calculus, each inequation states that the following abstraction invariant holds between the abstract variables a in A and the concrete variables b in B:
  (a=f(b)) and p(b)

But the main subject of [Ol92] is the SETS calculus functorial approach to data reification, which is so relevant and effective in the current version of the calculus and enables a generic approach to recursive data domain reification. In brief, the SETS functorial basis provides a structural view of abstraction invariant synthesis based on the following monotonicity result:

A <f,p B implies F(A) <F(f),F(p) F(B)

for every primitive or derived data construct F. Abstraction invariant handling was particularly at target in Jourdan's M.Sc. thesis [Jo92] on the foundations of SETS . Her ideas were adopted in handling so-called in loco invariants in SETS [Ol94e]. The categorial basis of invariant calculation is presented in [Ol98c]. Other work on SETS includes

• a SETS formalization of E-R diagrams [Ro93] [OC93];
• a data reification approach to relational database normalization theory [Ro93] [RO97b];
• a SETS -based strategy for data-model classification and reuse [OC93];
• using SETS for reuse in a reverse engineering context [NO95a].

As already shown in [Ol92], SETS combines easily with other calculi, such as Algebra of Programming or the Refinement Calculus . Monads and SETS are blended together in [Ba96a] to formalize the incorporation of a temporal dimension in database models. As can be found in [Ol97b] and [Ol98a], the functorial calculus of SETS supports the reasoning implicit in operation reification diagram solving.

Academic Context

SETS has been regularly taught at the University of Minho since 1989. The above cited work on relating relational database theory and SETS has been determinant in the way database design is taught to Minho's undergraduate students.

Normalized data models are easily obtained from formal specifications by SETS calculation (click here for a brief illustration). Final year projects usually involve the full calculation of an SQL information server running on top of ORACLE technology. (As an intermediate step in development, the formal specs are usually animated in the CAMILA rapid prototyping shell, see [ABNO97[a-c]]; mSQL (Mini SQL) has often been a target programming device, prior to the ORACLE final implementation.)

Industrial Application

Many students have reported the successful application of the calculus at industrial software design level. A list of industrial projects which resorted to program calculation in SETS is currently being compiled and will soon become available from this page.

SETS has been successfully applied in a number of projects, eg. SOUR (Eureka 379). An area in which SETS seems to exhibit some potential is that of (formal) reverse engineering, see eg. [Ol97f].

Currently, it is the formal basis of KARMA , an AdI -funded industrial contract signed (1998) with three software houses (NOVABASE Porto , NOVABASE Lisbon and SIDEREUS ) aiming at addressing Data Quality from novel perspectives. These include the use of formal methods and the adoption of formal techniques for data representation and (reverse) calculation of data intensive applications.

Documentation and Tools

By far, the most comprehensive account of the calculus is an as yet unpublished text book, currently in its 4th edition [Ol95d]. An English version should become available by the end of 1999. The lecture notes (Postscript ) of two courses on SETS technology are also available [Ol97b] [Ol98a]. See the Bibliography below.

A library of about fifty abstraction functions, written in the CAMILA executable formal notation, can be obtained from here .

The prospect of building SETS automated reification tools is discussed elsewhere . The on-going LOGCOMP project includes an integration of SETS with the COQ theorem prover.

The SETS Calculus Research Group

Current Members:

• J.N. Oliveira (Ph.D., Aux. Prof.) - currently interested in SETS -based point-free calculation and formal calculation of distributed applications.
• L.S. Barbosa (M.Sc., Lecturer) - currently finishing his Ph.D. on a SETS -based co-algebraic approach to agent-refinement calculus.
• C.J. Rodrigues (M.Sc., Lecturer) - currently doing a Ph.D. on relating SETS to other reification calculi.
• F.L. Neves (Lic., research assistant) - currently finishing an M.Sc. project on a SETS animator using genetic-algorithms to support term-rewriting.
• L.G. Ferreira (Lic.) - currently doing an M.Sc. project on a SETS -semantics for OLAP technology.

Past Members:

• C.G.Ferreira - she did an M.Sc. project on a SETS -based ``classify-by-data'' approach to software classification [Fe96].
• I.S. Jourdan - she did an M.Sc. project on the foundations of SETS [Jo92].

Bibliography

Comments on our papers and ideas are very welcome.

ABNO97a

J. J. Almeida, L. S. Barbosa, F. L. Neves, and J. N. Oliveira.
CAMILA: Formal software engineering supported by functional programming.
In A. De Giusti, J. Diaz, and P. Pesado, editors, Proc. II Conf. Latino Americana de Programación Funcional (CLaPF97 ), pages 1343-1358, La Plata, Argentina, October 1997. Centenario UNLP.

ABNO97b

J. J. Almeida, L. S. Barbosa, F. L. Neves, and J. N. Oliveira.
CAMILA: Prototyping and refinement of constructive specifications.
In M. Johnson, editor, Algebraic Methodology and Software Technology, pages 554-559. Springer LNCS, December 1997.
6th International Conference, AMAST'97 , Sydney, Australia, 13-17 December 1997, Proceedings.

ABNO97c

J. J. Almeida, L. S. Barbosa, F. L. Neves, and J. N. Oliveira.
Bringing CAMILA and SETS together -- the bams.cam and ppd.cam CAMILA Toolset demos.
Technical report, DI/UM, Braga, December 1997.
[45 p. doc.] .

Ba96a

L. S. Barbosa.
The monadic structure of time.
Technical report, Dep. Informática, University of Minho, 1996.

Ba97a

L. S. Barbosa.
A note on SETS functorial foundations, March 1997.
DI/UM Internal Research Note.

Fe96

C. Ferreira.
Uma abordagem formal ao problema da classificação de componentes de software.
Master's thesis, University of Minho, 1996.
(in Portuguese).

Jo92

I. S. Jourdan.
Reificação de tipos abstractos de dados: Uma abordagem matemática.
Master's thesis, University of Coimbra, 1992.
(In Portuguese).

NO95a

F. L. Neves and J. N. Oliveira.
Software Reuse by Model Reification .
In WISR'95 - 6th Annual Workshop on Software Reuse , August 28-30 1995.
Charles Il, Illinois, USA.

NO98

F. L. Neves and J. N. Oliveira.
ART -- Um Laboratório de Reificação «Genética».
In IBERAMIA'98 -- Sixth Ibero-Conference on Artificial Intelligence, pages 201-215, Lisbon, Portugal, October 5-9 1998.
(in Portuguese).

Ol84

J. N. Oliveira.
The Formal Semantics of Deterministic Dataflow Programs.
PhD thesis, Department of Computer Science, University of Manchester, Feb. 1984.

Ol87

J. N. Oliveira.
Refinamento transformacional de especificações (terminais).
In Actas das XII «Jornadas Luso-Espanholas de Matemática», volume II, pages 412-417, Braga, Portugal, 4-8 May 1987.

Ol90

J. N. Oliveira.
A Reification Calculus for Model-Oriented Software Specification .
Formal Aspects of Computing , 2(1):1-23, April 1990.

Ol92

J. N. Oliveira.
Software Reification using the SETS Calculus .
In Proc. of the BCS FACS 5th Refinement Workshop, Theory and Practice of Formal Software Development, London, UK, pages 140-171. Springer-Verlag, 8-10 January 1992.
(Invited paper).

Ol94e

J. N. Oliveira.
Hash Tables -- A Case Study in <,-calculation .
Technical Report DI/INESC 94-12-1, INESC Group 2361, Braga, December 1994.

Ol97f

J. N. Oliveira.
A calculational approach to reverse specification, 1997.
Seminar presented at UNU/IIST , Macau, May 13th, 1997, 22 p. [available as a 88K ps.gz file].

Ol95d

J. N. Oliveira.
Métodos Formais de Programação.
University of Minho, 4.th edition, 1997.
Textbook (489 p. in Portuguese [available as a 846K gzipped PS file]). English version under preparation at the time of writing.

Ol97b

J. N. Oliveira.
SETS -- a data structuring calculus and its application to program development.
Technical report, UNU/IIST , May 1997.
Lecture Notes of Course at UNU/IIST , Macau, 5-16 May 1997, 125p. [available as a 305K .ps.gz file].

Ol98a

J. N. Oliveira.
A data structuring calculus and its application to program development, May 1998.
Lecture Notes of M.Sc. Course (150 p. [available as a 390K gzipped PS file]). Maestria em Ingeneria del Software, Departamento de Informatica, Facultad de Ciencias Fisico-Matematicas y Naturales, Universidad de San Luis, Argentina.

Ol98b

J. N. Oliveira.
`Explosive' Programming Controlled by Calculation .
Technical Report UMDITR02/98, DI, University of Minho, September 1998.
Presented at AFP'98 (3rd Intern. Summer School on Advanced Functional Programming), Braga, Portugal.

Ol98c

J. N. Oliveira.
`Fractal' Types: an Attempt to Generalize Hash Table Calculation , 1998.
Presented at WGP98 , June 18, 1998, Marstrand, Sweden.

OC93

J. N. Oliveira and A. M. Cruz.
Formal calculi applied to software component knowledge elicitation.
Technical Report C19-WP2D, DI/INESC, December 1993.
IMI Contract C.1.9. Sviluppo di Metodologie, Sistemi e Servizi Innovativi in Rete. [available as a 167K ps.gz file].

R*98

J.V. Ranito, L.M. Henriques, L.M. Ferreira, F.L. Neves, and J.N. Oliveira.
Data quality: Do it formally?
In IASTED Conf. on Software Engineering (IASTED'98 (SE) ) Oct. 28-31, Las Vegas, USA, pages 260-262. Acta Press, Calgary - Zurich, 1998.

Ro93

C. J. Rodrigues.
Sobre o desenvolvimento formal de bases de dados.
Master's thesis, University of Minho, 1993.
(In Portuguese).

RO97b

C. J. Rodrigues and J. N. Oliveira.
Normalization is Data Reification .
Technical report, University of Minho, Dec. 1997.