We present a theory of software model preservation and isomorphism (enhancement) and proving correctness of model of reengineering using graph and set theory (GS). A lot of software applications will be in the legacy state every five years as a result of changes in technology and business processes. Modeling has become a de facto standard in software engineering. Developing, deriving from existing models, composing and proving correctness of models are part and parcel of the software development process. We describe a specification technique that combines the methods of adaptive modeling and model composition.

Model morphism, operational and failure consistencies, model composition, graphnet