Z-Specification-Based Query Answering System Standard Inspection

A query answering spec must prove the rigor of a specification after he has written it.Theorem proving can eliminate inconsistency of a specification so that the specification can be verified with respect to the user requirements.This paper validates the respect of requirements by formal method with Z language on initialization conditions and pre-conditions predigested of the conventional query answering question system,so the specification can meet the users' requirements.