Post condition example

Here follows an example of a post condition contract:

  @ContractReference(contractClassName = "DummyContract")
  public class Dummy
  {
    protected List m_stuff = new LinkedList();

    public int addItem(Object item)
    {
      m_stuff.add(item);
      return m_stuff.size();
    }
  }

  public class DummyContract extends ContractBase<Dummy>
  {
    public DummyContract(Dummy target)
    {
      super(target);
    }

    public void classInvariant()
    {
      assert m_target.m_stuff != null;
    }

    public void pre_addItem(Object item)
    {
      super.setPreconditionValue("list-size", m_target.m_stuff.size());
    }

    public void post_addItem(Object item)
    {
      assert m_target.m_stuff.contains(item);
      int preSize = super.getPreconditionValue("list-size");
      assert preSize == m_target.m_stuff.size() - 1;
      assert m_target.m_stuff.size() == super.getReturnValue();
    }
  }

By extending the ContractBase class, this post condition verifies both that the item actually has been added, that nothing else has been removed, and that the return value is the expected.