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

Question

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

http://jmlspecs.sourceforge.net/

С помощью:

• OpenJML
• Netbeans 7.3
• Java SDK 1.7

Я уже добавил файлы jar OpenJML в путь к классам NetBeans. я попробовал cofoga google jml-версию, куда вы просто импортируете com.google.java.contract.Ensures; импортировать com.google.java.contract.Requires, затем вы можете добавить предварительные и пост условия

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

Answer 1

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

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