Validity invariants and effects

摘要: Object invariants describe the consistency of object states, and are crucial for reasoning about correctness object-oriented programs. However, in presence abstraction encapsulation, arbitrary aliasing re-entrant method calls, is difficult.We present a framework based on behavioural contract that specifies two sets: validity invariant-- objects must be valid before after behaviour; effect--objects may invalidated during behaviour. The overlap these sets critical because it captures precisely those need to re-validated at end When there no overlap, further checking required.We also type system this using ownership types confine dependencies invariants. In order track invariant, restricts updates permissible contexts, even calls. referencing read access unrestricted, unlike earlier systems.