Using History Invariants to Verify Observers

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.

Using History Invariants(esop2007).pdf
PDF file

In  ESOP

Publisher  Springer

Details

TypeInproceedings
Pages80-94
Volume4421
SeriesLecture Notes in Computer Science
ISBN978-3-540-71314-2
> Publications > Using History Invariants to Verify Observers