Implementations Which are Definitions
Norman Foo · Australian Software Engineering Conference · 1991
There is a large class of implementations of abstract specifications which have the logical form of definitions. Thus relationship between an abstraction and its implementation can be viewed in two ways. The theory of the implementation can be regarded as a conservative extension of the theory of the abstraction, a viewpoint motivated by algebraic specifications. The Jones conditions for implementation correctness can be derived from this perspective. On the other hand the implementation may be regarded as given, and the abstraction viewed as the result of information hiding. This is the essence of specification extraction, and procedures to achieve it are investigated.