Abstract
We present a partial correctness proof system for ABS, an imperative, concurrent and object-oriented language which provides asynchronous communication model that is suitable for loosely coupled objects in the distributed setting. The proof system is derived from a standard sequential language by means of a syntactic encoding and applies Hoare rules. The execution of a distributed system is represented by its communication history, which can be predicated by history invariant. Modularity is achieved by establishing history invariants independently for each object and composed at need. This results in behavioral specification of distributed system in an open environment. As a case study we model and analyze the reader-writer example in the framework we developed.