gistfile1.java

package pl.xlab.doc.banana;

import com.google.java.contract.Ensures;
import com.google.java.contract.Invariant;
import com.google.java.contract.Requires;
import com.google.java.contract.ThrowEnsures;
import pl.xlab.doc.banana.exceptions.NotEnoughBananasException;

import java.util.Collection;

/** @author Konrad Malawski */
@Invariant("countBananas() >= 0")
public interface BananaService {

  @Requires({
                "amount > 0"
            })
  @Ensures({
               "countBananas() == old(countBananas()) - amount",
               "result != null"
           })
  @ThrowEnsures({
                    "NotEnoughBananasException", "countBananas() == 0"
                })
  public Collection<Banana> requestBananas(int amount) throws NotEnoughBananasException;

  @Ensures("old(countBananas()) == countBananas()")
  public void performInventory();

  public int countBananas();
}