Algebraic implementations preserve program correctness (Q1079358)

Algebraic specification of data types are a method for giving a precise formal description of the computation structures to be used in a software project. After the validation of an algebraic specification an implementation of these computation structures has to be developed, if the computation structures are to be used. In constrast to approaches where concrete models of data types are constructed it is suggested in this paper to replace an algebraic specification by another one which is closer to the computation structures available in the target machine or the target language. Correctness criteria are given that guarantee the preservation of partial or total correctness of programs when replacing the given algebraic specifications on which the programs operate by the new ones. This way the concept of algebraic implementations and their correctness is obtained. Moreover the transitivity of implementations is shown.