Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Using History Invariants to Verify Observers

K. Rustan M. Leino and Wolfram Schulte

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.

Details

Publication typeInproceedings
Published inESOP
Pages80-94
Volume4421
SeriesLecture Notes in Computer Science
ISBN978-3-540-71314-2
PublisherSpringer
> Publications > Using History Invariants to Verify Observers