There is an Open Access version for this licensed article that can be read free of charge and without license restrictions. The content of the Open Access version may differ from that of the licensed version.
Pricing information
Please choose your delivery country and your customer group
Considers the specification and verification of modules in hierarchically structured programs, as proposed by Parnas and Hoare. The author argues that a specification for such a module is a set of sentences in some logical language in which the names to be exported by the module appear as nonlogical symbols. He further argues that an implementation of one module in terms of another module is a translation of the nonlogical symbols of the first specification into the language of the second. Equality must also be interpreted. He proposes necessary conditions which any such notion of 'correct implementation' ought to satisfy. He then studies DLP, a specification language obtained by adding uninterpreted procedure symbols to Pratt's first order dynamic logic.