###
DOI:
Journal of Software:2000.11(3):285-292

时序逻辑语言XYZ/E中指针的形式化表示与验证
李广元,唐稚松
(中国科学院软件研究所计算机科学开放研究实验室,北京,100080;贵州大学计算机理论研究所,贵阳,550025)
Formalization and Verification of Pointers in the Temporal Logic Language XYZ/E Programs
LI Guang-yuan,TANG Zhi-song
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 3010   Download 2759
Received:March 27, 1998    Revised:November 01, 1998
> 中文摘要: 指针是一种重要的数据类型,使用指针能使程序更加有效和优美.可是指针却以不易驾御而闻名,至今在时序逻辑语言中未见到对它的形式化工作.XYZ/E既是一个时序逻辑系统也是一个程序设计语言,它能表示普通高级语言中几乎所有的重要机制.本文主要讨论在时序逻辑语言XYZ/E中指针的形式化表示问题以及在结构化XYZ/SE程序中指针的验证问题.
Abstract:Pointer is an important data type in most programming languages.It can make programs more efficient and more elegant.Unfortunately,this important concept is always notorious for its timelessness.Until now,no proper way to formalize it in temporal logic language has been found.XYZ/E is a temporal logic system as well as a programming language.It can represent almost every kind of significant features in conventional imperative languages.This paper is devoted to the representation of pointer in language XYZ/E and the verification of XYZ/SE programs with pointers.
文章编号:     中图分类号:    文献标志码:
基金项目:This research is suppouted by the National ‘Ninth-five’Sci-Tech Key Project of China(“九五”国家重点科技攻关项目计划,No.98-780-01-07-01). This research is suppouted by the National ‘Ninth-five’Sci-Tech Key Project of China(“九五”国家重点科技攻关项目计划,No.98-780-01-07-01).
Foundation items:
Reference text:

李广元,唐稚松.时序逻辑语言XYZ/E中指针的形式化表示与验证.软件学报,2000,11(3):285-292

LI Guang-yuan,TANG Zhi-song.Formalization and Verification of Pointers in the Temporal Logic Language XYZ/E Programs.Journal of Software,2000,11(3):285-292