时序逻辑语言 XYZ/E中指针的形式化表示与验证(英文)

作     者：李广元 唐稚松 LI Guang-yuan;TANG Zhi-song

作者机构：中国科学院软件研究所计算机科学开放研究实验室 贵州大学计算机理论研究所贵阳550025 

基　　金："九五"国家重点科技攻关项目计划!No.98- 780 - 0 1- 0 7- 0 1&& 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2000年第11卷第3期

页      码：285-292页

摘      要：指针是一种重要的数据类型 ,使用指针能使程序更加有效和优美 .可是指针却以不易驾御而闻名 ,至今在时序逻辑语言中未见到对它的形式化工作 .XYZ/E既是一个时序逻辑系统也是一个程序设计语言 ,它能表示普通高级语言中几乎所有的重要机制 .本文主要讨论在时序逻辑语言 XYZ/E中指针的形式化表示问题以及在结构化 XYZ/SE程序中指针的验证问题 .

主 题 词：形式语义 程序验证 指针 时序逻辑语言 XYZ/E 

学科分类：08[工学] 0835[0835] 0811[工学-水利类] 0812[工学-测绘类] 081202[081202] 

核心收录：

D　O　I：10.13328/j.cnki.jos.2000.03.001

馆 藏 号：203873050...