In practice, the formal development of software is an evolutionary process. Failed proof attempts give rise to changes in the specification and such changes invalidate proofs which have been previously performed. Clearly, it is very desirable to preserve much of the proof effort after such changes. In this paper, we propose development graphs as a general framework for modular specifications and define a structure preserving translation of CASL specifications into these graphs. The feature of development graphs, which is most important for an evolutionary process, is that they simplify the analysis of changes to the specification such that their negative effects can be kept to a minimum.
展开▼
