Razieh Piri - Computer Engineering Department Sharif University of Technology Azadi Ave., Tehran, Iran
Seyed-Hassan Mirian-Hosseinabadi - Assistant Professor Computer Engineering Department Sharif University of Technology Azadi Ave., Tehran, Iran

JML is a behavioral interface speci cation language which has Java as its target implementation language. It com- bines the idea of using Java expressions from Ei el lan- guage with the model-based approach to specify a pro- gram. Re nement calculus is a framework to produceexecutable code from a speci cation by preserving the correctness of programs. In this paper some constructs of JML concerning object creation, feature call, excep- tional behavior and concurrency constructs are studied and some re nement rules are proposed to obtain an object oriented code in Java from a JML speci cation containig these constructs. The correctness of these rules is proved by weakest precondition predicate trans- former. The re nement of usual constructs in JML such as If-statement, Loop and Assignment from pre- vious works such as Z re nement is also demonstrated.

Formal Methods, Speci cation, Ob- ject Oriented, JML, Re nement Rule, Weakest Pre- condition