Formal representation of reuseable software modules

Recovering design information from software is an active research area in reverse engineering. If the extracted information is represented formally, we are able to process the information at the semantic level for analysis and reasoning. We describe a formal approach to representing modules. A module encapsulates a collection of dependent components. The main feature of the formalism is characterized by its underlying operational semantics. This allows us to execute the specification of a module and to simulate its behavior. A homogeneous algebra is used for representing a module. The type hierarchy of certain modules is represented by means of a lattice. A lattice can be transformed into an executable form easily, such as to a frame notation in a knowledge representation system. The properties, of the operations or the functions in a module, are described by characteristic assertions which result from certain relationships between the operations. In our formalism, the properties are represented by Horn clauses. A set of Horn clauses provides a capability to check the behavior of a module