Refactoring in Maintenance and Development of Z Specifications and Proofs

AbstractOnce you have proved your refinement correct, that is not the end. Real products, and their accompanying specifications, develop over time, with new improved versions having added functionality. There are new maintenance issues that arise when altering and upgrading pre-existing large specifications and their respective proofs.We show how concepts from refactoring can be used to structure this process, and provide a means for well-defined, disciplined modifications. Additionally, we discuss how the analogy between proof and refactoring, as meaning preserving transforms, can be used to suggest the development of a refactoring toolset, and thence a refinement toolset