|
|||||
|
|
| 用于C语言程序验证的性质描述语言C-PDL | |
| 引用本文： | 左春华,张广泉,郭亮.用于C语言程序验证的性质描述语言C-PDL[J].苏州大学学报(医学版),2007,23(3):31-36. |
| 作者姓名： | 左春华 张广泉 郭亮 |
| 作者单位： | [1]苏州大学计算机科学与技术学院,江苏苏州215006 [2]中国科学院软件研究所,北京100080 |
| 摘 要： | 为了保证程序的正确性,可以先将程序抽象成模型,再采用模型检测技术对模型进行验证.模型检测工具只接受形式化的性质描述语言,而一般程序员很难正确地使用,因此,文章提出了半形式化的描述语言C-PDL,并介绍了采用C-PDL描述性质的验证系统.C-PDL采用时序逻辑语言XYZ/AE的语法结构,结合了C语言程序性质的特点,引入规范模式系统,其语法简单且描述能力强.另外,C-PDL表达式可以方便地转换成模型检测工具识别的各种时序逻辑公式. |
| 关 键 词： | 规范模式系统 程序性质 模型检测 |
| 文章编号： | 1000-2073（2007）03-0031-06 |
| 收稿时间： | 2006-10-22 |
| 修稿时间： | 2006年10月22 |
| 本文献已被 维普 万方数据 等数据库收录！ | |