Formalization and Verification of Pointers in the Temporal Logic Language XYZ/E Programs
时序逻辑语言XYZ/E中指针的形式化表示与验证

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.