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 mathematical characterization 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 threadspsila 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 Hepsilas Unifying Theories of Programming(UTP) [2] and at same time extends it.