Like other software engineering activities, formal modelling needs to deal with change: bugs and omissions need to be corrected, and changes from the outside need to be dealt with. In the context of axiomatic specifications and (partly) interactive proofs, the main obstacle is that changes invalidate proofs, which then need to be rebuilt using an inhibitive amount of resources. This thesis proposes to solve the problem by considering the state of a formal development consisting of (potentially buggy) specification and (potentially partial) proofs as one entity and transforming it using preconceived transformations. These transformations are operationally motivated: how would one patch the proofs on paper given a consistent transformation for the specification? They are formulated in terms of the specification and logic language, so as to be usable for several application domains.weiterlesen