| 摘要: |
| 本文提出了一个简单的方法，其中程序和其性质都由一个逻辑：时序逻辑中的公式表示．文中给出了一个程序的转换模块的定义，提出了时序执行语义的概念．它是一个时序公式，精确地说明了一个程序．将时序逻辑作为规范语言，程序正确性就意味着说明程序的公式蕴含说明性质的公式，其中蕴含即为一般的逻辑蕴含．因此，本文的方法为并发程序的规范及验证提供了一个统一的框架．它允许充分利用现有的用于证明并发系统时序性质的各种完全证明系统．一个缓冲系统的简单例子用来说明本文的方法．此例子表明本文的方法是可行的. |
| 关键词: 程序验证 规范 程序正确性 时序逻辑 证明系统 缓冲系统 |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到博士点基金资助. |
|
| A UNIFIED FRAMEWORK FOR PROGRAM VERIFICATION |
|
JIA Guoping,ZHENG Guoliang
|
| Abstract: |
| This paper presents a simpler approach in which both a program and its properties are specified by formulas in the same logic: the temporal logic. A transition module of a program is defined and the notion of temporal run semantics, which is a temporal formula precisely characterizing the program is presented. Taken temporal logic as specification language, the correctness of a program means that the formula specifying the program implies the formula specifying the property, where implies is ordinary logical implication. Therefore this approach gives a unified framework for specifying and verifying concurrent programs and allows a full utilization of the existing comprehensive proof systems developed for proving temporal properties of systems. A simple example of a buffer system is presented to illustrate this method and show that the approach is very promising. |
| Key words: Program verification specification correctness of a program temporal logic proof system a buffer system |
