An approach for refining JML specification to object oriented code

JML is a behavioral interface specification language which has Java as its target implementation language. It combines the idea of using Java expressions from Eiffel language with the model-based approach to specify a program. Refinement calculus is a framework to produce executable code from a specification by preserving the correctness of programs. In this paper some constructs of JML concerning object creation, feature call, exceptional behavior and concurrency constructs are studied and some refinement rules are proposed to obtain an object oriented code in Java from a JML specification containing these constructs. The correctness of these rules is proved by weakest precondition predicate transformer. The refinement of usual constructs in JML such as If-statement, Loop and Assignment from previous works such as Z refinement is also demonstrated.