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

${\displaystyle {\mbox{Register}}_{k}:={\mbox{Register}}_{k}+1}$,

${\displaystyle {\mbox{Register}}_{k}:={\mbox{Register}}_{k}{\dot {-}}1}$

and the test

${\displaystyle {\mbox{Register}}_{k}=0?}$,

in which

${\displaystyle x{\dot {-}}1={\begin{cases}x-1,&{\mbox{wenn}}\,x>0\ \\0,&{\mbox{sonst}}\end{cases}}}$

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