Z规格说明的前置条件的简化

摘要

在软件方法学中，形式方法越来越受到人们的重视，并已被应用于软件开发。Ｚ是一种基于数学表示的软件规格说明方法。前置条件的简化是Ｚ规格说明方法中一种标准的检查，本文讨论了Ｚ规格说明中关于操作的前置条件及其计算，提出了简化过程的终止条件，给出了一个有于简化前置条件的算法，该算法可自动产生简化过程的证据。