形式化方法是一种用数学方法来描述和验证目标软件系统性质的方法，它通常用形式规格说明语言来描述软件需求。由于用数学符号描述的软件规格说明比较抽象，而且是不可执行的，因此非专业人员不太容易理解，很难判断所给出的规格说明是否与他们的需求一致。这就需要对规格说明进行确认。本文研究的规格说明的动画模拟就是一种规格说明的确认方法，它将不可执行的规格说明转换成一种可执行的程序，用户执行转换后的程序，根据执行后的反馈信息判断该规格说明是否符合他们的需求。 由于SQL在动画模拟中的诸多优点，因此在本文的研究中将SQL作为动画模拟Obiect-Z规格说明的目标语言。从Object-Z到SQL的转换是本文的研究重点，本文利用两种语言之间的相似性，制定了相应的转换规则，提出了利用数据表表示各种类型的数据变量的方法；并提出模块封装的思想，即用存储过程表示类、对象和模式等模块，用户通过调用执行存储过程确认规格说明是否满足其需求。 在动画模拟过程中首先需要进行规格说明语言到SQL语言的转换。通常动画模拟都是针对规格说明的某个部分进行的，因此就没必要对整个规格说明转换，只需要提取相关的部分即可。为此，本文提出了分层的规格说明切片方法，并将它运用于规格说明的动画模拟中，提高了动画模拟的效率和准确性。 本文还讨论了用XML描述Obiect-Z规格说明的方法，根据动画模拟的特点用XML Schema分别对规格说明中的变量和各种模块定义了格式，使规格说明的描述格式尽量为动画模拟带来方便。 最后根据研究的方法开发了一个规格说明的动画模拟工具，该工具可以自动将用户输入的规格说明转换成SOL程序，并将执行转换后的结果显示在界面上，以方便用户对规格说明的一致性做出判断。