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

作者：李广元; 唐稚松

来源：软件学报, 2000, (03): 285-292.

• 时序逻辑
• 形式语义
• 程序验证
• 动态语义
• 指针 Temporal logic
• formal semantics
• program verification
• dynamic semantics
• pointer.

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

• 出版日期2000
• 单位中国科学院软件研究所; 贵州大学