###
DOI:
Journal of Software:1997.8(2):107-114

一个统一的程序验证框架
贾国平,郑国梁
(南京大学计算机科学系,南京,210093; 南京大学计算机软件新技术国家重点实验室,南京,210093)
A UNIFIED FRAMEWORK FOR PROGRAM VERIFICATION
JIA Guoping,ZHENG Guoliang
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 2276   Download 2903
    Revised:January 26, 1996
> 中文摘要: 本文提出了一个简单的方法,其中程序和其性质都由一个逻辑:时序逻辑中的公式表示.文中给出了一个程序的转换模块的定义,提出了时序执行语义的概念.它是一个时序公式,精确地说明了一个程序.将时序逻辑作为规范语言,程序正确性就意味着说明程序的公式蕴含说明性质的公式,其中蕴含即为一般的逻辑蕴含.因此,本文的方法为并发程序的规范及验证提供了一个统一的框架.它允许充分利用现有的用于证明并发系统时序性质的各种完全证明系统.一个缓冲系统的简单例子用来说明本文的方法.此例子表明本文的方法是可行的.
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.
文章编号:     中图分类号:    文献标志码:
基金项目:本文研究得到博士点基金资助. 本文研究得到博士点基金资助.
Foundation items:
Reference text:

贾国平,郑国梁.一个统一的程序验证框架.软件学报,1997,8(2):107-114

JIA Guoping,ZHENG Guoliang.A UNIFIED FRAMEWORK FOR PROGRAM VERIFICATION.Journal of Software,1997,8(2):107-114