An Approach for Re ning JML Speci cation To Object Oriented Code

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.

Keywords:

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