用于C语言程序验证的性质描述语言C-PDL

C-PDL:a property description language of C based on specification patterns system

为了保证程序的正确性,可以先将程序抽象成模型,再采用模型检测技术对模型进行验证.模型检测工具只接受形式化的性质描述语言,而一般程序员很难正确地使用,因此,文章提出了半形式化的描述语言C-PDL,并介绍了采用C-PDL描述性质的验证系统.C-PDL采用时序逻辑语言XYZ/AE的语法结构,结合了C语言程序性质的特点,引入规范模式系统,其语法简单且描述能力强.另外,C-PDL表达式可以方便地转换成模型检测工具识别的各种时序逻辑公式.

In order to assure the program correct,we can abstract the program to a model by program properties and then verify the model by Model Checkers.Model Checkers just accept formal description languages for properties.Programmers are hard to use.So the article brings forward the language C-PDL and explains the structure of the verifying system in C-PDL.C-PDL is the integration of XYZ/AE and the Specification Patterns System.And the C program＇s characters are taken into account.It＇s easy and powerful.The formulas in C-PDL can easily be translated into all kinds of temporal logic formulas that Model Checkers accept.