Transformations of specifications and proofs to support an evolutionary formal software development

Abstract

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 dealtwith. 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. In order to make the approach compatible with the architecture of existing support systems, development graphs are added as an intermediate concept between specification and proof obligations, and the transformations are extended to work in the presence of the indirection. This leads to a separation of a framework for propagating transformations through development graphs and a reference instantiation that commits to concrete languages and proof representation. The reference instantiation works for many practically relevant scenarios. Other instantiations can be based on the framework.