Anzeige
Erschienen in:
2001 | OriginalPaper | Buchkapitel
Computability and Complexity Results for a Spatial Assertion Language for Data Structures
verfasst von : Cristiano Calcagno, Hongseok Yang, Peter W. O’Hearn
Erschienen in: FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
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
This paper studies a recently developed an approach to reasoning about mutable data structures, which uses an assertion language with spatial conjunction and implication connectives. We investigate computability and complexity properties of a subset of the language, which allows statements about the shape of pointer structures (such as “there is a link from x to y”) to be made, but not statements about the data held in cells (such as “x is a prime number”). We show that validity, even for this restricted language, is not r.e., but that the quantifierfree sublanguage is decidable. We then consider the complexity of model checking and validity for several fragments.