摘要： ＰＶＳ是斯坦福研究机构开发的强大的规约、验证系统，它的适用领域广泛。在概要介绍ＰＶＳ的构成、功能后，着重分析了ＰＶＳ的规约语言、验证系统的特点，以及使得ＰＶＳ灵活、强大的设计决策和内在机制．

关键词: 规约语言, 定理证明器, 形式化方法

Abstract: PVS is a powerful specification and verification system developed by Stanford Research Inshtute, its application area is broad. After briefly introducing the composition and function of PVS, this paper puts great emphasis on analyzing the features of PVS'specification language, verification system and design decisions, as well as inner mechanisms that make PVS powerful and flexible.

中图分类号: 

• TP311