|
|||||
|
|
| 程序性质的描述与证明 | |
| 引用本文： | 官荷卿,郭亮.程序性质的描述与证明[J].计算机科学,2003,30(3):146-148. |
| 作者姓名： | 官荷卿 郭亮 |
| 作者单位： | 中国科学院软件研究所计算机科学开放研究实验室,北京,100080 |
| 基金项目： | 国家自然科学基金YCK15028 |
| 摘 要： | XYZ/E是一种基于Manna-Pnueli线性时序逻辑的线性时序逻辑语青(LTLL),其主要特征为它在统一的时序逻辑框架下既能表示程序的静态规范(XYZ/AE)也能表示可执行代码(XYZ/EE),因此程序规范和程序可执行代码的语义一致性也就得以在时序逻辑框架下验证。对于顺序程序,XYZ系统提供了一套基于Hoare逻辑规则的验证工具XYZ/VERI。此工具通过读取程序及其前后断 |
| 关 键 词： | 程序性质 程序设计 XYZ语言 AE语言 时序逻辑语言 |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |
| 点击此处可从《计算机科学》下载全文 | |
