Flexible Immutability with Frozen Objects

摘要: Object immutability is a familiar concept that allows safe sharing of objects. Existing language support for based on immutable classes. However, class-based approaches are restrictive because programmers can neither make instances arbitrary classes immutable, nor they control when an instance becomes immutable. These restrictions prevent many interesting applications where objects mutable go through number modifications before become immutable. This paper presents flexible technique to enforce the individual by transferring their ownership special freezer object, which prevents further modification. The demonstrates how facilitates program verification extending Boogie methodology object invariants Spec#'s dynamic ownership, but concepts also apply other systems transfer.