在计算机科学领域中，程序分析足一种自动化地分析计算机程序的行为的重要技术。程序分析技术主要应用于程序的优化和程序正确性验证两个方面。现代编译器常常会利用程序分析技术对程序源代码的分析结果来实现公共子表达式删除、死代码删除、循环优化等一系列代码优化策略。而在形式化方法中占据重要地位的模型检测技术也常常会与程序分析技术相结合来验证程序的安全性、活性等重要性质。　　 当前，程序分析领域的一个重要课题是如何自动化地分析程序中的数组所满足的性质。数组是计算机程序中最常见的数据结构之一，几乎所有大型的计算机程序都包含数组以及对数组的操作。早在上世纪七十年代，关于数组越界检查的程序分析技术就已被提出，并且已经在Java等程序语言中得到了成功的应用。但是关于数组内容的程序分析技术直到最近才得到广泛地研究。其主要原因在于一个数组在理论上可以包含无限多的数组元素，而一般的静态程序分析技术在面对数组时可能会因为数组元素过多而使分析程序无法终止。因此，现有的程序分析技术需要经过扩展来处理程序中的数组。　　 抽象解释是基于有序集合上的单调函数来对程序的语义做和谐逼近的理论。它可以被看做是通过对计算机程序的部分执行来获取程序的语义信息的方法。本文提出一种将抽象解释和程序分析技术相结合的方法来对程序中的数组及其上的操作进行分析，并自动发现数组的某些数值性质，比如数组中所有元素的取值范围。本文的主要工作是将P.Cousot和R.Cousot提出的基于区间抽象域对程序进行抽象解释的方法扩展到包含数组操作的程序中。为了满足数组分析的需要，我们将首先对经典的区间抽象域进行扩展，在其上定义了两个新的操作。然后利用规范抽象方法给出基于扩展的区间抽象域的数组程序分析算法。通过对几个常用的包含数组操作的程序进行的分析，表明本文提出的算法可以快速找到程序语义的上界逼近，并通过此逼近自动证明这些程序中数组所满足的重要性质。