集合共享的_soundness_、_idempotence_与_commutativity
编程语言
2007-05-23 v1
摘要
实际的数据流分析器必须以可靠的理论结果为依据。抽象解释提供了一种 soundness的数学框架和抽象域所需的通用属性，以确保其相对于具体语义的良定义性和 soundness。 在逻辑编程中，共享域是共享分析的标准选择，适用于实际工作和进一步的理论研究。尽管如此，我们发现没有对共享关键属性的满意证明，这些属性对于共享的良定义性至关重要，而且已发表的共享 soundness 声明假设存在occurs-check。本文提供了一个可适用于任何语言（无论是否具有occurs-check）的抽象函数通用化。本文证明了使用该抽象函数进行抽象统一的 soundness、idempotence和commutativity。
引用
@article{arxiv.cs/0102030,
title = {Soundness, Idempotence and Commutativity of Set-Sharing},
author = {Patricia M. Hill and Roberto Bagnara and Enea Zaffanella},
journal= {arXiv preprint arXiv:cs/0102030},
year = {2007}
}
备注
48 pages