摘要：PAR平台是本团队研制成功的支撑软件形式化和自动化开发的软件平台。该平台充分体现了功能抽象和数据抽象的优越性,使得软件开发变得便捷和可靠,达到这一性能的关键要素是一批可重用软件构件。为保证整个软件平台的正确性和可靠性,确保其中软件构件的正确性和可靠性就显得十分重要。选取PAR平台中若干典型软件构件,用形式化方法对构件的语义进行形式化描述,并借助Coq定理证明系统,对构件的正确性进行形式化验证,大幅度提高了软件构件形式化验证的效率。

关键词：软件构件 形式语义 定理证明 par平台 循环不变式 

单位：江西师范大学国家网络化支撑软件国际科技合作基地; 江西南昌330022; 江西省高性能计算技术重点实验室; 江西南昌330022