Target members

To be able to implement good contracts, the contract needs access to the targets member fields (this is at least true for in-house testing, however, to verify libraries that e.g. are used by clients you may only want to use the publicly available information about your components).

If you pass in the target reference to the ContractBase constructor, you will be able to get access to private fields in the target using the "Object getTargetField(String fieldName)" method, as shown below:

  public class SomeContract extends ContractBase<Some>
  {
    public SomeContract(Some target)
    {
      super(target);
    }

    public void classInvariant()
    {
      assert ((List)super.getTargetField("m_stuff")).size() > 0;
      assert ((List)super.getTargetField("m_stuff")).
        get(0).equals("boho");
    }
  }

To avoid casting in your contract implementations, I would recommend to create a typed getter for each target field you are going to access, like this:

  public class SomeContract extends ContractBase<Some>
  {
    public SomeContract(Some target)
    {
      super(target);
    }

    public void classInvariant()
    {
      getStuff().size() > 0;
      getStuff().get(0).equals("boho");
    }

    private List getStuff()
    {
      return (List)super.getTargetField("m_stuff");
    }
  }