摘要
本文提出了一个简单的方法,其中程序和其性质都由一个逻辑:时序逻辑中的公式表示.文中给出了一个程序的转换模块的定义,提出了时序执行语义的概念.它是一个时序公式,精确地说明了一个程序.将时序逻辑作为规范语言,程序正确性就意味着说明程序的公式蕴含说明性质的公式,其中蕴含即为一般的逻辑蕴含.因此,本文的方法为并发程序的规范及验证提供了一个统一的框架.它允许充分利用现有的用于证明并发系统时序性质的各种完全证明系统.一个缓冲系统的简单例子用来说明本文的方法.
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.
出处
《软件学报》
EI
CSCD
北大核心
1997年第2期107-114,共8页
Journal of Software
基金
博士点基金
关键词
程序验证
规范
程序正确性
Program verification, specification, correctness of a program, temporal logic, proof system, a buffer system.