Formal Multi-threading Method of Object-Oriented

For improving the reliable, safe, and high quality software, object-oriented multi-threading software become more and more. This paper presented a mathmatical charaterization of multi-threading object-oriented semantics, supply rCOS [1] theory such as abstract method, final method and synchronized method. Consider object lock, thread waiting, synchronized method, provide a algebra method to describe threads' executing, which proves the method is valid to specify multi-threading and verify multi-threading object-oriented system. The method call of thread is base on the pre-condition logic in Hoare and He's Unifying Theories of Programming(UTP) [2] and at same time extends it.