Compositional Reasoning of Concurrent Objects with Asynchronous Method Calls
Johan Dovland
Current object-oriented approaches to distributed programs may be criticized in several respects. First, method calls are generallysynchronous, which leads to much waiting in distributed and unstable networks. Second, the common model of thread concurrency makes reasoning about program behavior very challenging. A model based on concurrent objects communicating by means of asynchronous method calls has been proposed to combine object orientation and distribution in a more satisfactory way.
In this talk we consider a reasoning system for this model, focusing on simplicity and modularity. We believe that a simple and compositional proof system is paramount to allow verification of real programs. The proposed proof rules are derived from the Hoare rules of a standard sequential language by means of a semantic encoding preserving soundness and relative completeness.