Proving Implementations Correct - Two Alternative Approaches

TitleProving Implementations Correct - Two Alternative Approaches
Publication TypeConference Paper
Year of Publication1980
AuthorsEhrich, H. - D.
Conference NameIFIP Congress 1980
PublisherNorth-Holland Publ. Comp.

Motivated by the desire to prove imnlementations correct, we present two approaches to making
the fundamental notion of implementation as a relationship between data types precise. The
first one captures the idea of simulation, while the second one, being more constructive in
nature, formalizes the idea of constructing on a given basis in distinguished steps something
isomorphic to a given target structure. Both approaches give rise to corresponding proof
methods which are demonstrated in examples. The approaches are shown to be equivalent as
far as the existence of implementations is concerned.

1980IFIP.pdf384.86 KB