Maintaining formal specifications - Decomposition of large Z-specifications

Being part of different maintenance models formal specifications can act as valid artefacts for maintenance tasks. However, the linguistic density of specification languages and the size of specifications might still be seen as an obstacle against comprehension, reuse, and change activities. This paper introduces an approach for the identification of specification fragments of Z specifications with a well defined semantic content. These fragments, namely specification chunks and specification slices, not only support comprehension tasks, they also enable maintenance personnel to identify and focus on the relevant parts of specifications for the problem at hand. Their ease in creation and use makes them well suited for maintenance, as is demonstrated by a simple prototype for Z specifications.