Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic
Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic
复制标题
使用多分类逻辑将数据结构与不稳定无限理论相结合
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
C. Zarba
中科院分区：
文献类型：
--
作者：
Silvio Ranise;C. Ringeissen;C. Zarba
大多数计算机程序将给定性质的元素存储到基于容器的数据结构中，例如列表，数组，集合和多重集合。为了验证这些程序的正确性，需要将联合收割机（theory S）与理论T（theory T）结合起来，理论S对数据结构进行建模，理论T对元素进行建模。只有当S和T都是稳定无穷大时，才能使用经典的Nelson-Oppen方法实现这种组合。
本文的目的是放松稳定的无限性要求。为了实现这一目标，我们引入礼貌理论的概念，我们表明礼貌理论的自然例子包括那些建模数据结构，如列表，数组，集合和多集。此外，我们提供了一种方法，能够联合收割机一个礼貌的理论S与任何理论T的元素，无论T是否是稳定无限的。
本文将Tinelli和Zarba最近关于单类逻辑中闪耀理论与非稳定无限理论的结合的结果推广到多类逻辑。
Most computer programs store elements of a given nature into container-based data structures such as lists, arrays, sets, and multisets. To verify the correctness of these programs, one needs to combine a theory S modeling the data structure with a theory T modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both S and T are stably infinite.
The goal of this paper is to relax the stable infiniteness requirement. To achieve this goal, we introduce the notion of polite theories, and we show that natural examples of polite theories include those modeling data structures such as lists, arrays, sets, and multisets. Furthemore, we provide a method that is able to combine a polite theory S with any theory T of the elements, regardless of whether T is stably infinite or not.
The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of shiny theories with nonstably infinite theories in one-sorted logic.