Design by contract - JML

Design by contract is a method for developing software. It's a contract between a client and it's class. The client must accept certain conditions before calling a method defined by the class (preconditions ) and the class must ensure certain properties after the call (postconditions) What is JML ? JML stands for "Java Modeling Language". You can specify both the syntactic interface of Java code and it's behaviour

The precondition and postconditions are written starting with an at-sign. To specifiy the client's clauses it has to agree upon we use the JML annotation @requires To say what must be true at the end of the method we use the @ensures clause.