Hierarchical program specification and verification — a many-sorted logical approach

The notion of abstractions in programming is characterized by the distinction between specification and implementation. As far as the specification structures are concerned, hierarchical program development with abstraction mechanisms is naturally regarded as a process of theory extensions in a many-sorted logic. To support such program development, a language called t is proposed with which one can structuredly build up theories and write their program implementation. There, the implementation is regarded as another level of theory extension, and the relation between the specification and the implementation of an abstraction is characterized in terms of a homomorphism between the two theories. On this formalism, a mechanizable proof method is introduced for validation of implementations of both data and procedural abstraction. Finally, a new data type concept is introduced to generalize the so-called type-parametrization mechanism. A justification of this concept within the first order logic is provided as well as its applications to program structuring and verification.