THE SIMPLIFICATION OF PRECONDITION IN Z SPECIFICATIONS
Z规格说明的前置条件的简化

In software methodology, formal methods is being paid more and more atten-tion and has been applied to software development. Z is a kind of software specification notations based on mathematics. The simplification of precondition is a standard check for Z specifications. This paper discusses the precondition in Z specifications and its calcula-tion, proposes a termination condition for sirnplifying the precondition and presents a sim-plifying algorithm which can automatically produce the justifications during the process of simplifying precondition.