Using History Invariants to Verify Observers
This talk delves into utilizing history invariants for verifying observers, emphasizing the importance of specifying and statically verifying programs, along with supporting common programming patterns. It covers subjects like observer and subject patterns, modular verification, invariants in data structures, and more.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Using history invariants to verify observers K. Rustan M. Leino and Wolfram Schulte Microsoft Research, Redmond ESOP 2007 Braga, Portugal 28 March 2007
Overall goal Specify and statically verify programs Use modular verification (local reasoning) These require: Invariants of data structures Support for common programming patterns
In this talk: Observer pattern Observer Subject Observer Observer
In this talk: Observer pattern or: Collection / Iterator pattern Iterator Collection Iterator Iterator
Review of the heap logic of the Boogie methodology class C { int x, y; invariant x y; void M() { expose (this) { x++; P(); y++; } } Invariant checked here Object is valid Object is mutable Program invariant: ( o o.valid Inv(o))
Review: Representation (rep) objects class FastDictionary { rep Dictionary d; rep Cache c; :Fast- Dictionary d c :Dictionary :Cache invariant contents = d.contents c.keys contents; Program invariant, for any rep field d: ( o o.valid o.d.valid)
Review: Visibility-based invariants class Node { Node next, prev; invariant (next = null next.prev = this) (prev = null prev.next = this); next next next :Node :Node :Node :Node prev prev prev
Subject, observers class Subject { int data; List<Observer> observers; } interface Observer { void Update(); } class MyObserver : Observer { Subject s; int d; invariant d = s.data; } class YourObserver : Observer { Subject s; int d; invariant d s.data; } :MyObserver Note that s cannot :MyObserver :Subject be a rep field, because one observer cannot be the sole owner of the subject :YourObserver
Modular verification problem :MyObserver class Subject { int data; List<Observer> observers; void Inc() { expose (this) { data++; foreach (o in observers) { o.Update(); } } } } interface Observer { void Update(); } :MyObserver :Subject :YourObserver Program invariant: ( o o.valid Inv(o))
Modular verification problem class Subject { int data; List<Observer> observers; void Inc() { expose (this) { expose (all o in observers) { data++; foreach (o in observers) { o.Update(); } } } } } interface Observer { void Update(); } :MyObserver :MyObserver :Subject :YourObserver or check the observer update guards here? How to check invariants of the observers here?
Our solution Declare (monotonic) evolution of the subject data: class Subject { int data; history invariant old(data) data; and let observer invariants depend on the subject data, provided these invariants are automatically maintained under the evolution of the subject data: class SomeObserver : Observer { subject Subject s; int data; invariant data s.data;
History invariants 2-state predicates history invariant R(this) , ; Holds of ordered pairs of states: valid Program invariant: ( , ( o R(o) , )) Program invariant: ( , ( o [o.valid] [o.valid] R(o) , ))
Checking history invariants Checked to be reflexive and transitive Checked in the states that bracket expose statements: expose (o) { } Check R(o) , here
Observer invariants class Subject { history invariant R(this) , ; } class Observer { subject Subject s; invariant Inv(this); Program invariant: ( o o.valid o.s.valid Inv(o)) expose (o) { } check o.s.valid Inv(o) here
Checking observer invariants class Subject { history invariant R(this) , ; } class Observer { subject Subject s; invariant Inv(this); Checked to satisfy: ( , ( o [o.valid] ( f [o.f] = [o.f] ) [o.s.valid] [o.s.valid] R(o.s) , [Inv(o)] ))
Soundness theorems Program invariant, for any history invariant R: ( , ( o [o.valid] [o.valid] R(o) , )) Program invariant, for any object invariant Inv: ( o o.valid o.s.valid Inv(o)) Proofs: see paper
Specification idiom class Subject { int ver; T data; history invariant old(ver) = ver old(data) data; class Observer { subject Subject s; int ver; T data; invariant s.ver = ver s.data data; temporal relation spatial relation
Example: Iterator class Iterator { int ver; subject Collection c; invariant ... c ...; T Next() requires this.valid c.valid this.ver == c.ver; { ... }
Related work History invariants are used elsewhere assume / guarantee constraints [Liskov & Wing 1994] Visibility-based invariants [e.g., Leino & M ller 2004] Update guards [Barnett & Naumann 2004] Separation logic [e.g., Parkinson & Bierman 2005] could also benefit from history invariants Static class invariants [Leino & M ller 2005] multiple- owner situation
Conclusion Local reasoning for observer invariants Future work: implementation (in Spec#)
