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 logic subsumes boolean algebra and includes (function) image expressions. Full assertion language is quite expressive, e.g., assertions can be quantified, however, its restriction to quantifier-free (QF) assertions yields a decidable theory.;Our thesis maintains that the logic is amenable to automation. To that end we implement an automated verifier for region logic; the verifier computes verification conditions which are first-order formulas. The verifier is used to specify and verify a suite of programs including those aforementioned. We also study, i.e., formalize and prove correct, decision procedures for QF assertions. We implement a semi-decision procedure integrated with a (satisfiability modulo theories) solver. To test its feasibility, we compare the implementation with an axiomatization based on quantified formulas; preliminary results are very encouraging. For a restricted language, we give an NP-complete decision procedure and prove its correctness.