摘要
抽象解释由CousotP和CousotR于1977年提出,随后许多作者做了大量工作.从不同的角度构造了基于部分等价关系和逻辑部分等价关系一个模型,它与传统抽象解释模型根本不同,该模型并不是对具体系统在"近似"意义上的抽象,而是对原系统上的一切关系(包括逻辑关系)的抽象,因此它不是原系统的"简化",而是原系统的一个"深化".从而在此模型上提出的问题具有另外的特征,例如复杂性和多态性等问题.
Abstract interpretation was presented by CousotP and CousotR in 1977.Subsequently many scholars have done a lot of studies on it.Generally speaking,the classic abstract interpretation theory is developing within two equivalent formal frameworks of Galois connections and closure operators.This paper constructs a model based on partial equivalence relations and logical partial equivalence relations from a different perspective.It considers the abstract domain as a collection of＂partial equivalence relations＂and the semantic operator as a collection of＂logical partial equivalence relations＂.So this model is totally different from the traditional abstract interpretation models.Except that it requires that the concrete or abstract semantic operators have certain logical relations,the model never requires some special properties such as the monotonicity,so in this point it is different from the classic model.Besides,it is not an abstraction of a concrete system in an＂approximate＂sense,but rather an abstraction of all relations（including logical relations）on the original system.Thus this model is not a＂simplification＂of the original system but rather a＂complication＂of the original system.In some sense,it disjoins the＂quality＂unit from the original system,and it may be more complex than the original system.The advantage of this model is that it embodies some logical relations concerned with the system functions,because the condition such as concrete or abstract semantic operations have any special properties（e.g.monotonicity）is not required.Therefore,the abstraction is not as the classic understanding.The classic way is to treat some approximation of states as an abstraction,and require that both concrete semantic domains and abstract semantic domains have certain special mathematical structure,for example,lattice or cpo,that is the result of treating＂approximation＂as the basic essence of abstraction.Whereas,our model help structure a concrete system from the semantic domain and the semantic operation the two parts by using partial equivalence relations and logical partial equivalence relations,i.e.,it extracts their components separately and finally forms the collection of equivalence classesto discuss the semantic domain and semantic operators.Also,based on such a model,we can discuss the issues that are different from the traditional models,such as the complexity problem and the polymorphism problems,so that it may deepen our understanding for the abstract interpretation theory.
出处
《南京大学学报（自然科学版）》
CAS
CSCD
北大核心
2015年第2期453-457,共5页
Journal of Nanjing University（Natural Science）
基金
国家自然科学基金(61170071)
金陵科技学院科研基金(jit-n-201305)
关键词
抽象解释
部分等价关系
逻辑部分等价关系
abstract interpretation
partial equivalence relation
logical partial equivalence relation
