Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
Reducing Lookups for Invariant Checking
verfasst von : Jakob G. Thomsen, Christian Clausen, Kristoffer J. Andersen, John Danaher, Erik Ernst
Erschienen in: ECOOP 2013 – Object-Oriented Programming
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
This paper helps reduce the cost of invariant checking in cases where access to data is expensive. Assume that a set of variables satisfy a given invariant and a request is received to update a subset of them. We reduce the set of variables to inspect, in order to verify that the invariant is still satisfied. We present a formal model of this scenario, based on a simple query language for the expression of invariants that covers the core of a realistic query language. We present an algorithm which simplifies a representation of the invariant, along with a mechanically verified proof of correctness. We also investigate the underlying invariant checking problem in general and show that it is co-NP hard, i.e., that solutions must be approximations to remain tractable. We have seen a factor of thirty performance improvement using this algorithm in a case study.