%0 Journal Article
%T A UNIFIED FRAMEWORK FOR PROGRAM VERIFICATION<br>一个统一的程序验证框架
%A JIA Guoping
%A ZHENG Guoliang
%A <br>贾国平
%A 郑国梁
%J 软件学报
%D 1997
%I 
%X 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.
%K Program verification
%K specification
%K correctness of a program
%K temporal logic
%K proof system
%K a buffer system<br>程序验证
%K 规范
%K 程序正确性
%K 时序逻辑
%K 证明系统
%K 缓冲系统
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=EA29C861AED85A2D0EC6EA2E40FD82FB&yid=5370399DC954B911&vid=5D311CA918CA9A03&iid=0B39A22176CE99FB&sid=D767283A3B658885&eid=DDD31293A7C7D057&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=25