Verifiable Programming of Object-Oriented and Distributed Systems

Abstract Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. This paper explores a programming paradigm based on active, concurrent objects communicating by so-called asynchronous method calls giving rise to efficient interaction by means of nonblocking method calls, implemented by means of message passing. The paradigm facilitates invariant specifications over the locally visible communication history of each class. Compositional reasoning is supported by rules comparable to those of sequential programming, and global properties may be derived from local specifications. Reasoning about inheritance is not limited by behavioral subtyping, but allowing free reuse of code, considering also multiple inheritance. A small, illustrating example is considered.