The SETS Calculus Home Page | |
---|---|

[ DI/UM ] |

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

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

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

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.

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.

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

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

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.

7/10/1999

Jose Nuno Oliveira