We encode arrays as functions which, in turn, are encoded as sets of ordered pairs. The set cardinality of each of these functions coincides with the length of the array it is representing. Then we define a fragment of set theory that is used to give the specifications of a non-trivial class of programs with arrays. In this way, array reasoning becomes set reasoning. Furthermore, a decision procedure for this fragment is also provided and implemented as part of the {log} (read 'setlog') tool. {log} is a constraint logic programming language and satisfiability solver where sets and binary relations are first-class citizens. The tool already implements a few decision procedures for different fragments of set theory. In this way, arrays are seamlessly integrated into {log} thus allowing users to reason about sets, functions and arrays all in the same language and with the same solver. The decision procedure presented in this paper is an extension of decision procedures defined in earlier works not supporting arrays.

翻译：我们将数组编码为函数，而函数又被编码为有序对集合。每个函数的集合基数与其所表示的数组长度一致。随后，我们定义一个集合论片段，用于描述一类包含数组的非平凡程序的规约。通过这种方式，对数组的推理转化为对集合的推理。此外，我们还为该集合论片段提供了一种判定过程，并将其作为{log}（读作'setlog'）工具的一部分实现。{log}是一种约束逻辑编程语言和可满足性求解器，其中集合和二元关系被视为一等公民。该工具已实现了针对不同集合论片段的多个判定过程。通过这种方式，数组被无缝集成到{log}中，从而允许用户在同一语言和同一求解器中对集合、函数和数组进行推理。本文提出的判定过程是对早期不支持数组的决策过程的扩展。