Flexible Invariants through Semantic Collaboration
Skip to main content
eScholarship
Open Access Publications from the University of California

Flexible Invariants through Semantic Collaboration

  • Author(s): Polikarpova, Nadia
  • Tschannen, Julian
  • Furia, Carlo A
  • Meyer, Bertrand
  • et al.

Published Web Location

https://arxiv.org/abs/1311.6329
No data is associated with this publication.
Abstract

Modular reasoning about class invariants is challenging in the presence of dependencies among collaborating objects that need to maintain global consistency. This paper presents semantic collaboration: a novel methodology to specify and reason about class invariants of sequential object-oriented programs, which models dependencies between collaborating objects by semantic means. Combined with a simple ownership mechanism and useful default schemes, semantic collaboration achieves the flexibility necessary to reason about complicated inter-object dependencies but requires limited annotation burden when applied to standard specification patterns. The methodology is implemented in AutoProof, our program verifier for the Eiffel programming language (but it is applicable to any language supporting some form of representation invariants). An evaluation on several challenge problems proposed in the literature demonstrates that it can handle a variety of idiomatic collaboration patterns, and is more widely applicable than the existing invariant methodologies.

Many UC-authored scholarly publications are freely available on this site because of the UC's open access policies. Let us know how this access is important for you.

Item not freely available? Link broken?
Report a problem accessing this item