通过程序变换实现数组和映射的简单抽象
编程语言
2015-06-16 v1 计算机科学中的逻辑
摘要
我们提出了一种处理数组程序的静态分析方法，该方法在数组程序的语义与纯标量运算的语义之间建立了伽罗瓦连接。实现它的最简单方法是通过自动的语法变换将数组程序转换为标量程序，然后使用任何静态分析技术（抽象解释、加速、谓词抽象等）对标量程序进行分析。这样得到的标量不变量被转换回原始程序，成为全称量化的数组不变量。我们在各种示例上说明了我们的方法，包括“荷兰国旗”算法。
引用
@article{arxiv.1506.04161,
title = {A simple abstraction of arrays and maps by program translation},
author = {David Monniaux and Francesco Alberti},
journal= {arXiv preprint arXiv:1506.04161},
year = {2015}
}