基于时间逻辑的程序正确性验证

摘要	第1-5页
Abstract	第5-8页
1 绪论	第8-15页
·研究背景	第8-12页
·程序验证概述	第8-11页
·运用编译技术的优点	第11-12页
·国内外研究发展与现状	第12-13页
·本文研究目的及主要工作	第13-14页
·论文章节安排	第14-15页
2 时间逻辑	第15-21页
·时间逻辑语言	第15-16页
·归结原理	第16-21页
·子句集	第17页
·命题逻辑中的归结原理	第17-18页
·替换与合一	第18页
·谓词逻辑中的归结原理	第18-21页
3 程序设计语言的公理语义	第21-41页
·类型定义的语义	第21-23页
·变量定义的语义	第23-24页
·运算符和表达式的语义	第24-28页
·语句的公理语义	第28-36页
·函数定义的公理语义及函数规范	第36-37页
·函数调用的公理语义	第37-39页
·有关公理	第39-41页
4 翻译 C程序成时间逻辑公式的过程	第41-59页
·词法分析	第42-46页
·语法分析	第46-53页
·语法分析技术	第47-49页
·语法分析的实现	第49-52页
·BISON输出程序的分析	第52-53页
·语义分析	第53-56页
·语义分析概述	第53-56页
·语义分析实现	第56页
·符号表	第56-59页
5 基于时间逻辑的程序验证	第59-68页
·一般原理	第59-61页
·验证实例	第61-64页
·证明模式	第64-68页
结论	第68-69页
参考文献	第69-71页
攻读硕士学位期间发表学术论文情况	第71-72页
致谢	第72-73页