KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > com > tirsen > nanning > contract > ContractIntf


1 package com.tirsen.nanning.contract;
2
3 /**
4  * Always need to use this-reference, jexl doesn't support "default"-variable.
5  *
6  * @invariant getValue() > 0
7  */

8 public interface ContractIntf {
9     public int getValue();
10
11     public void setValue(int value);
12
13     /**
14      * "{old this.method()}" will be executed before the invocation of the method but used in the
15      * post-condition. Variables are named #arg0, #arg1, #arg2 and so on... (in wait for new features of Nanning
16      * attributes which could perhaps handle this better.)
17      *
18      * @requires #arg0 > 0
19      * @ensures {old getValue()} + #arg0 == getValue()
20      */

21     public void increaseBy(int value);
22 }
23
Popular Tags