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 sDecifications．This paper discusses the precondition in Z specifications and its calcula-tion. Droposes a termination condition for simplifying the precondition and presents a sim-plifying aIgorithm which can automatically produce the justifications during the process of simplifying precondition．