Invariants for Non-Hierarchical Object Structures

摘要: We present a Hoare-style specification and verification approach for invariants in sequential OO programs. It allows over non-hierarchical object structures, which update patterns that span several objects methods occur frequently. This gives rise to invalidating subsequent re-establishing of way compromises standard data induction, assumes hold when method is called. provide constructs (inc coop) identify involved such patterns, allowing refined form induction. The now handles practical designs, as illustrated by the Observer Pattern.