Skip to main content
Conference ProceedingsOPEN ACCESS

Using history invariants to verify observers

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2007) 4421 LNCS 80-94
DOI: 10.1007/978-3-540-71316-6_7
22Citations
Citations of this article
4Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

This paper contributes a technique that expands the set of object invariants that one can reason about in modular verification. The technique uses history invariants, two-state invariants that describe the evolution of data values. The technique enables a flexible new way to specify and verify variations of the observer pattern, including iterators. The paper details history invariants and the new kind of object invariants, and proves a soundness theorem. © Springer-Verlag Berlin Heidelberg 2007.

Cite

CITATION STYLE

APA

Leino, K. R. M., & Schulte, W. (2007). Using history invariants to verify observers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4421 LNCS, pp. 80–94). Springer Verlag. https://doi.org/10.1007/978-3-540-71316-6_7

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free