Interpolation is an essential tool in software verification, where first-order theories are used to constrain datatypes manipulated by programs. In this paper, we introduce the datatype theory of contiguous arrays with maxdiff, where arrays are completely defined in their allocation memory and for which maxdiff returns the max index where they differ. This theory is strictly more expressive than the array theories previously studied. By showing via an algebraic analysis that its models strongly amalgamate, we prove that this theory admits quantifier-free interpolants and, notably, that interpolation transfers to theory combinations. Finally, we provide an algorithm that significantly improves the ones for related array theories: it relies on a polysize reduction to general interpolation in linear arithmetics, thus avoiding impractical full terms instantiations and unbounded loops.
翻译:内插是软件核查的一个基本工具, 使用一阶理论来限制程序操纵的数据类型。 在本文中, 我们引入了数据类型理论 : 以最大尺寸排列的连续数组, 数组在分配内存中被完全定义, 最大值返回最大值指数, 其数值不同。 这个理论比先前研究的数组理论更严格地表达。 通过代数分析显示其模型高度合并, 我们证明该理论承认无量化的内插, 特别是内插转换为理论组合。 最后, 我们提供了一种大大改进相关数组理论的算法: 它依赖于将多尺度缩小到线性计算中的一般性内插, 从而避免不切实际的全术语的瞬间和无界圈。