Refinement (computer science)
In computer science, refinement is a process in which a more concrete description is derived from an abstract description (e.g. register machine , formal specification using Z notation ). A refinement receives (certain) properties of the abstract description in the concrete description.
Refinement in register machines
In theoretical computer science, refinement is understood to be a process for constructing correct, simple register machines from generalized register machines.
Simple register machine
The simple register machine only knows the commands
- ,
and the test
- ,
in which
is the arithmetic difference.
This definition of subtraction ensures that one remains within the natural numbers .
Register machines for further functions
If you have now written a register machine that is able to add two numbers a and b, for example, then you can in future add two registers directly in each register machine: Instead of this direct addition, you could also use the register machine for adding two numbers a and insert b.
This step is called refinement.
A register machine that needs to be refined is called a generalized register machine.
meaning
The refinement makes it easier to specify a clear, legible and short register machine for a function. An example shows the proof of the predictability of the Cantor pairing function .
literature
- Klaus Weihrauch: Computability . Springer, Berlin et al. 1987, ISBN 3-540-13721-1 , ( EATCS monographs on theoretical computer science 9).
- Katrin Erk, Lutz Priese: Theoretical Computer Science. A comprehensive introduction . 2nd expanded edition. Springer, Berlin et al. 2002, ISBN 3-540-42624-8 , ( Springer textbook ).
- Uwe Schöning : Theoretical Computer Science - Briefly , 4th Edition. Corrected reprint. Spectrum, Heidelberg et al. 2003, ISBN 3-8274-1099-1 , ( university paperback ).