// a list of Object values
public /*@ pure @*/ class ListModel
{
  // create empty list
  // default constructor ListModel();

  // the length of this list
  //@ public model int length();

  // the element of this list at position i
  //@ public model Object get(int i);

  // true if this list equals the given list
  //@ public model boolean equals(ListModel list);

  // the result of appending to this list an element
  //@ public model ListModel append(Object e);

  // the concatenation of this list with another list
  //@ public model ListModel append(ListModel list);

  //@ axiom new ListModel().length() == 0;

  /*@ axiom 
    @   (\forall ListModel list1, list2; list1 != null && list2 != null;
    @     list1.equals(list2) <==>
    @       list1.length() == list2.length() &&
    @       (\forall int i; 0 <= i && i < list1.length();
    @          list1.get(i) == list2.get(i)));
    @*/

  /*@ axiom 
    @   (\forall ListModel list; list != null;
    @     (\forall Object e; ;
    @        list.append(e) != null &&
    @        list.append(e).length() == 1+list.length() &&
    @        (\forall int i; 0 <= i && i < list.length();
    @          list.append(e).get(i) == list.get(i)) &&
    @        list.append(e).get(list.length()) == e));
    @*/

  /*@ axiom 
    @   (\forall ListModel l1, l2; l1 != null && l2 != null; 
    @     l1.append(l2) != null &&
    @     l1.append(l2).length() == l1.length() + l2.length() &&
    @     (\forall int i; 0 <= i && i < l1.length(); 
    @        l1.append(l2).get(i) == l1.get(i)) &&
    @     (\forall int i; l1.length() <= i && i < l1.length()+l2.length(); 
    @        l1.append(l2).get(i) == l2.get(i-l1.length())));  
    @*/
}