多年以来，形式化规约(formal specification)一直是软件工程领域中的一个研究热点，它的应用范围也正在逐步增长。一般来说，形式化规约是用形式化语言编写的系统规格说明，是系统的属性在某种级别上的抽象表示，能够提供系统行为的精确描述。不过，大型复杂系统的形式化规约在可读性上总是不能令人满意，有时候甚至是规约的编写人员自己都无法知道规约是否定义了“应有的行为”。为解决这个问题，人们提出了规约示范（Specification animation）技术。它通过直接或间接地对规约进行解释和执行来提供一种模拟机制，将规约的行为展示给用户或规约开发人员，帮助他们理解规约。此外，规约示范技术可以和规约验证和校验（specification verification and validation）方法结合起来使用，以达到更好的规约验证效果。 本文提出了一种针对SOFL (Structured Object-oriented Formal Language)规约的规约示范方法并讨论了支持这一方法的工具——SOFL-Animator的设计和开发。SOFL-Animator在规约示范的过程中使用消息序列图（MSC）来显示每条序列的执行过程，从而更好地表现规约中各个部分之间的交互。同时，它还提供对规约示范的过程支持，按照特定的覆盖策略抽取出规约的典型执行序列，然后依次对每一条序列进行示范。用户可以在工具的引导下系统地对规约行为进行示范。 本文的工作在一定程度上克服了SOFL规约在可读性上的缺陷，为SOFL规约的验证和校验提供支持。同时本文提出的方法是第一个针对SOFL的规约示范方法，而SOFL-Animator也是目前为止第一款支持SOFL规约示范的工具，它在过程支持和透明性上有着不错的表现。