Once 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.
Full paper : PDF 229K | doi: 10.1016/S1571-0661(05)80485-2
@inproceedings(SS-REFINE02,
author = "Susan Stepney and Fiona Polack and Ian Toyn",
title = "Refactoring in Maintenance and Development of
{Z} Specifications and Proofs",
pages = "396--415",
crossref = "REFINE02"
)
@proceedings(REFINE02,
title = "REFINE 2002, BCS-FACS Refinement Workshop,
Copenhagen, Denmark, July 2002",
booktitle = "REFINE 2002, BCS-FACS Refinement Workshop,
Copenhagen, Denmark, July 2002",
editor = "John Derrick and Eerke Boiten and Jim Woodcock
and Joakim von Wright",
series = "ENTCS",
volume = 70,
number = 3,
publisher = "Elsevier",
year = 2002
)