Taxonomy/2. Methodology
In the precious chapters we started from the question how one can establish beyound reasonable doubt that something is the case and investigated the rôle of mathematics in a rational approach. We then investigated what this means for the construction of artefacts that must do what they are supposed to do. We concluded the investigation with quality criteria.
The next chapters switch from understanding to methodology. How should we proceed of we want to contruct and understand artefacts?
Ideally, we should...
- specify the desired properties,
- validate the specification,
- derive a blueprint from the specification by some method that guarantees that that blueprint satiefies the specification (e.g. Monotonic Refinement),
- realise the artefact by some procedure that guarantees that the result is a correct realisation of the blueprint.
In practice, development consits a mix of creation, evolution and construction. The problem is more or less well-defined, and what is given varies. To make it worse, many "paradigms", languages, methods, and tools have been developed to support (parts of) this chaotic process. Not all of them are theoretically well-founded. This problem is in the focus of Computer Science research: Methods and tools to support professional activities should be based on sound theories. When these methods and tools manipulate formal objects, these should be written in well-defined languages that have suitable properties. Computer Science has brought forward many good theories, languages, methods, and tools for the construction and analysis of artefacts that must do what they are supposed to do.
But it is not always clear how to choose from that great variety. Often, it is not even clear, what the problem is that has to be solved.
Therefore we propose to depart from a Problem Statement that defines what the problem is, what is given and what has to be found in which domain.
Furthermore, we propose to let the development process be guided by a good unterstanding of what a Correctness Theorem is.
