| On the Design of a «Periodic Table» of VDM Specifications |
|---|---|
| [ DI/UM ] |
Abstract: Formal modelling is advocated as a means of capturing and reasoning about the knowledge embodied in (the solution to) a problem. If performed at the right level of abstraction, using a mathematically tractable notation, it represents a significant step towards reliable software description able to endure arbitrary technology change. Still the question arises at abstract level: how much is «new» in a model when compared to others already available? Put in other words: where is the borderline between invention and sheer routine work in formal modelling?
Domain analysts try to answer these questions by structuring specification repositories according to problem areas. Still it is often the case that the model one is looking for can only be found in another problem area, if stripped from its domain-specific terminology. There is a need to investigate alternative internal structures for formal model repositories able to unveil their mathematical essence and spot model "intersection" in a systematic way.
This talk describes work which, in this spirit, tries to restructure a corpus of standard algorithmic knowledge written in VDM notation. Algorithms are classified and catalogued in a tabular structure according to their formal specification. Every algorithmic model is subject to a «Laplace-like» transformation which identifies its underlying polynomial structure and inductive behaviour. Each polynomial gives rise to a row in the table and captures a particular «efficiency» pattern. Columns in the table correspond to abstract classes of problems (e.g. setify, square, sort, count), that is, to polytypic program schemata. «Holes» in the table correspond to (often «new») algorithms and can be filled in by inter-combining and shifting around the elementary components of the available specifications. These are identified by factorization techniques using the relational hylomorphism calculus. So, algorithms are «triples» (F,a,c) where a and c -- resp. an algebra/coalgebra of polynomial relator F -- behave as the «genetic» material of the corresponding algorithm, which can be recovered by transformation back to the pointwise level.
This approach underlies the way algorithmics are taught at Minho and is the basis of a program understanding discipline to be developed in the PURE reverse engineering project.