Object Invariants in Dynamic Contexts K. R. M. Leino and P. Muller



Yüklə 475 b.
tarix17.11.2018
ölçüsü475 b.


Object Invariants in Dynamic Contexts

  • K.R.M. Leino and P. Muller

  • 15-819: Objects and Aspects

  • Presented by Jonathan Aldrich


Outline

  • Problem

    • Modular enforcement of invariants
    • Separate reasoning with callbacks and inheritance
  • Solution

    • Class invariants
    • Partial packing and unpacking
    • “Ownership” relation
  • Discussion



Callbacks and Invariants

  • class T {

  • int a, b ;

  • invariant 0 <= a < b

  • public 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 m


Inheritance and Invariants

  • class Derived extends Base {

  • int a, b ;

  • invariant 0 <= a < b

  • public 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 scope


Class Invariants

  • class 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



Class Invariants

  • class 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…



Class Invariants

  • class 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…



Class Invariants

  • class 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…



Class Invariants

  • class 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…



Inheritance and Invariants

  • class Derived extends Base {

  • int a, b ;

  • invariant 0 <= a < b

  • public void m(. . .) {

  • unpack this from Derived

  • int k := 100/(b - a) ;

  • super.m(. . .) ; // unpacks and re-packs Base

  • a := a +3 ; P(. . .) ; b := (k + 4) . b ;

  • pack this as Derived

  • }

  • }

  • Incremental unpacking and re-packing supports modular verification



Callbacks and Invariants

  • class T {

  • int a, b ;

  • invariant 0 <= a < b

  • public 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 packed


Invariants and Sub-objects

  • class 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-objects

  • class 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 unpacked


Ownership Transfer

  • transferable 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


  • explain visibility rules

  • field update rules



Discussion

  • Practicality

    • Requires very careful tracking of containing object state
    • Forbids iterators, etc.
    • Strong conditions for transfer
  • Lessons for informal reasoning?

  • Applicability to aspects?




Dostları ilə paylaş:


Verilənlər bazası müəlliflik hüququ ilə müdafiə olunur ©genderi.org 2017
rəhbərliyinə müraciət

    Ana səhifə