Object Invariants in Dynamic ContextsOutlineCallbacks and InvariantsInheritance and InvariantsClass InvariantsSlide 6Slide 7Slide 8Slide 9Slide 10Slide 11Invariants and Sub-objectsOwnership, Boogie StyleSlide 14Ownership TransferIs “ownership” really Ownership?Slide 17DiscussionObject Invariantsin Dynamic ContextsK.R.M. Leino and P. Muller15-819: Objects and AspectsPresented by Jonathan AldrichOutline•Problem–Modular enforcement of invariants–Separate reasoning with callbacks and inheritance•Solution–Class invariants–Partial packing and unpacking–“Ownership” relation•DiscussionCallbacks and Invariantsclass T {int a, b ;invariant 0 <= a < bpublic T( ) { a := 0 ; b := 3 ; }public void m(. . .) {int k := 100/(b - a) ;a := a +3 ; P(. . .) ; b := (k + 4) . b ;}}•What if P calls m?–Soundness: Must ensure it doesn’t, or that the invariant is not assumed by mInheritance and Invariantsclass Derived extends Base {int a, b ;invariant 0 <= a < bpublic void m(. . .) {int k := 100/(b - a) ;super.m(. . .) ;a := a +3 ; P(. . .) ; b := (k + 4) . b ;}}•What about the invariants of Base?–Modularity: would like to assume that super call ensures them–Need notion entering and leaving a class scopeClass Invariantsclass C extends B { int w ;invariant w < 100 ; . . . }class B extends A { int z ;invariant y < z ; . . . }class A extends object { int x, y ; invariant x < y ; . . . }•inv = A–Invariant A must hold–B and C may or may not holdC: w = 43B: z = 6A: x = 5 y = 7object:inv = AClass Invariantsclass C extends B { int w ;invariant w < 100 ; . . . }class B extends A { int z ;invariant y < z ; . . . }class A extends object { int x, y ; invariant x < y ; . . . }o.z = y+1;pack o as B;pack o as C;continue…C: w = 43B: z = 6A: x = 5 y = 7object:inv = AClass Invariantsclass C extends B { int w ;invariant w < 100 ; . . . }class B extends A { int z ;invariant y < z ; . . . }class A extends object { int x, y ; invariant x < y ; . . . }o.z = y+1;pack o as B;pack o as C;continue…C: w = 43B: z = 8A: x = 5 y = 7object:inv = AClass Invariantsclass C extends B { int w ;invariant w < 100 ; . . . }class B extends A { int z ;invariant y < z ; . . . }class A extends object { int x, y ; invariant x < y ; . . . }o.z = y+1;pack o as B;pack o as C;continue…C: w = 43B: z = 8A: x = 5 y = 7object:inv = BClass Invariantsclass C extends B { int w ;invariant w < 100 ; . . . }class B extends A { int z ;invariant y < z ; . . . }class A extends object { int x, y ; invariant x < y ; . . . }o.z = y+1;pack o as B;pack o as C;continue…C: w = 43B: z = 8A: x = 5 y = 7object:inv = CInheritance and Invariantsclass Derived extends Base {int a, b ;invariant 0 <= a < bpublic void m(. . .) {unpack this from Derivedint k := 100/(b - a) ;super.m(. . .) ; // unpacks and re-packs Basea := a +3 ; P(. . .) ; b := (k + 4) . b ;pack this as Derived}}•Incremental unpacking and re-packing supports modular verificationCallbacks and Invariantsclass T {int a, b ;invariant 0 <= a < bpublic T( ) { a := 0 ; b := 3 ; }public void m(. . .) requires this . inv = T {unpack this from T ;int k := 100/(b - a) ;a := a +3 ; P(. . .) ; b := (k + 4) . b ;pack this as T ;}}•What if P calls m?–It must first restore the invariant and pack this as T, because m’s precondition assumes that T is packedInvariants and Sub-objectsclass BTree {int i ;BTree left, right ;invariant (left != null)  left.i < i (right != null)  right.i ≥ i ;}•How to ensure invariant modularly?–What if someone modifies left.i without going through the current object?Ownership, Boogie Style•p is owned by o at T–p.owner = [o,T]•p is committed–p.committed•All invariants hold for committed objects–p.committed  p.inv = type(p)•Object is committed when owner is packed–p.owner = [o,T]  (p.committed  o.inv ≤ T)Invariants and Sub-objectsclass BTree {int i ;rep BTree left, right ;invariant left.owner = [this, BTree] ;invariant right.owner = [this, BTree] ;invariant (left != null)  left.i < i (right != null)  right.i ≥ i ;}•Invariant can rely on owned objects–unpack this, invariants hold for children–children can’t be unpacked (and thus can’t have broken invariants) unless owner is first unpackedOwnership Transfertransferable class Possession {. . .}class Person {rep Possession possn ;void donateTo(Person p)requires ¬committed È inv = Person ;requires possn = nullÈ Ètype(possn) = Possession ;requires p = null È p = this È ¬p.committed È p.inv = Person ;modifies possn, p.possn ; {unpack this from Person ; unpack p from Person ;unpack possn from Possession ;transfer possn to [p, Person] ;pack possn as Possession ;p.possn := possn ; pack p as Person ;possn := null ; pack this as Person ;}. . .}Is “ownership” really Ownership?•Ownership in Boogie–Allows external aliases (but can’t mutate through them)–Supports ownership transfer–Heavyweight: must track precisely•Classical Ownership–External aliases–No ownership transfer–Lightweight: can track with typesI find this all a bit misleading…probably better to use a different term•explain visibility rules•field update rulesDiscussion•Practicality–Requires very careful tracking of containing object state–Forbids iterators, etc.–Strong conditions for transfer•Lessons for informal reasoning?•Applicability to