摘要
作为别名分析的主要形式,指向分析通过计算指向关系提供完整的别名关系。准确刻画指向分析中相关概念及语义十分有助于深入理解程序中指向关系的生成及变化过程,并为别名分析或指向分析相关形式化工作奠定理论基础。针对面向对象程序设计语言中一个与指向分析有关的基本子集,给出指向关系和指向状态的数学描述,定义一个指向分析语义函数PT以刻画面向对象程序中基本语句对指向状态的作用。最后证明了该语义是合适定义的。
As a main form of alias analysis, points-to analysis provides complete alias relation by computing the points-to relationship. Accurate depiction of correlated notions and semantics of points-to analysis is very helpful for morethoroughly understanding the generation and change processes of points-to relations in the program, and lays a theoretic base for the related formal analyses in regard to alias analysis or points-to analysis. Aiming at a basic subset pertaining to points-to analysis in object-oriented programming language, we give the mathematical description for points-to relation and points-to state, and define a points-to analysis semantics function PT to depict the role of basic statements of an objective program on points-to states ; Finally we prove that the semantics is appropriate for the definition.
出处
《计算机应用与软件》
CSCD
2015年第2期5-9,17,共6页
Computer Applications and Software
基金
国家自然科学基金项目(61262029)
贵州省自然科学基金项目(20122021)
关键词
指向分析
语义
合适定义
证明
Points-to analysis
Semantics
Well-definedness
Proof
