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.

کلیدواژه ها:

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