Constructive consistency checking for partial specification ln Z

摘要

Partial specification is a method of specifying complex systems in which the system is de- scribed by a collection of specifications, each approaching the system from a different viewpoint. The specification notation Z is often advocated as a suitable language for this style of specifi- cation. For collections of partia1 specifications to be meaningful, they need to be consistent, i.e. they should not impose contradictory requirements. This paper addresses how the consistency between partial specifications in Z can be checked, by constructing unifications, i.e. least com- mon refinements, of viewpoint specifications.