Как мы применяем JML (openJML) к Java-коду?

Question

Как применить JML к Java-коду? Я все еще новичок в дизайне по контрактам и совершенно потерял, как применить его в программе.

http://jmlspecs.sourceforge.net/

Использование:

• OpenJML
• Netbeans 7,3
• Java SDK 1.7

Я уже добавил опарника OpenJML в пути к классам Netbeans , Я попробовал версию cofoga google jml, где вы просто import com.google.java.contract.Ensures; импорт com.google.java.contract.Requires , то вы можете добавить предварительно и постусловие

Как мы определяем заранее состояние и после условия с использованием openJML в моей программе?

Answer 1

Я нашел то, что нужно; импортирует библиотеку с аннотациями:

import org.jmlspecs.annotation.Requires; 
import org.jmlspecs.annotation.Ensures;