Design by contract - JML

Seite 1

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.