摘要
时序逻辑作为一种规格说明语言,能够很好地描述程序性质.为了能够利用现有的定理证明器PVS(prototype verification system)对用时序逻辑公式描述的程序性质予以证明,从而达到程序验证的目的.文中在PVS中建立了时序逻辑的语义模型,同时给出了其语义解释.然后通过一个简单的例子(求解整数平方根的程序),应用时序逻辑公式对该程序的部分性质进行了描述,取得了较好的效果.实现了程序性质的时序逻辑公式表示,为使用PVS验证程序的性质打下了一个好的基础.
As a specification language , temporal logic is powerful enough in expressing the properties for program. In order to prove the theorem that expresses the property （PVS）, this paper establishes a semantics model for using temporal logic formula in a prototype verification system temporal logic as well as the semantics interpretation. As an example, a program for solving the square root for an integer is investigated. Some properties of this program are in temporal logic formulas. An interface for verifying program by PVS is orovided. specified
出处
《应用科学学报》
CAS
CSCD
北大核心
2006年第6期598-603,共6页
Journal of Applied Sciences
基金
国家自然科学基金(60173031)
国家"973"重点基础研究发展计划(2002CB312001)资助项目
