Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic
verfasst von : Silvio Ranise, Christophe Ringeissen, Calogero G. Zarba
Erschienen in: Frontiers of Combining Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.