PROVING THE EXISTENCE OF INITIAL STATE IN Z SPECIFICATIONS
Z规格说明中初始状态存在性的证明

Proof of the initialization theorem is a standard check that may be carried out for any state-based specification. A procedure for proving initialization theorems is presented. The proof justifications can be generated automatically by this procedure. By way of example, two initialization theorems are proved using this procedure.