Treffer: 0429894. REGION LOGIC: LOCAL REASONING FOR JAVA PROGRAMS AND ITS AUTOMATION

Shared mutable objects are a cornerstone of the object-oriented paradigm. The ability to share mutable data eliminates unnecessary cloning and gives rise to efficient data structures. Yet, formal reasoning about partial correctness of object-oriented programs is notoriously difficult due to the very same features, viz., sharing and mutable objects. The core problem is aliasing, and one of the contributions of this thesis is a program logic designed to control aliasing through explicit use of effects and disjointedness assertions. We propose a straightforward adaptation of Hoare logic to reason about (sequential) Java programs. The logic employs regions (sets of references) in a novel way, by using them in ghost state, effects and assertions. The aptly named—region logic—embodies “local reasoning ” as witnessed by separation logic, without resorting to non-standard semantics or higher-order constructs. Region logic is formalized (and proven sound) with respect to a core subset of Java. Several illustrative examples including subject/observer and composite design patterns are specified and proven partially correct. The assertion language of region